- Research News
- Contact Us
- Department Life
- Oral History of Cornell CS
- Department Timeline
- Annual Reports
- Job Postings
- Ithaca Info
- Internal info
- CS Colloquium
- CU Tech Colloquium
- BOOM 2017
- SoNIC Workshop
- Conway-Walker Lecture Series
- Salton Lecture Series
- Seminars / Lectures
- Big Red Hacks
- 50th Anniversary Symposium
- Cornell University High School Programming Contest
- Game Design Initiative
- SJTU International Workshop
Programming Languages is a lively area at Cornell with eight faculty and over a dozen Ph.D. students. We are proud of both our breadth and depth in this core discipline. Cornell has been known from the beginning for its research in programming languages. We have made foundational contributions to type theory, automated theorem proving, and language semantics. A more recent theme has been language-based solutions to important problems such as computer security, networking, and distributed programming. Cornell researchers have also contributed to language implementation, program analysis and optimization, domain-specific languages, and software engineering.
Erik Andersen explores how programming language concepts can be utilized in the service of education. He is interested in how the relative difficulty of practice problems for learning a procedural skill (e.g. subtraction) can be estimated by analyzing the procedural execution trace obtained by executing the target procedure on a practice problem. He is currently applying this technique to math, video games, programming, and human language. He is also interested in how program synthesis can help explain what students are doing when they become confused, having recently showed that many misconceptions in math can be modeled and diagnosed in this way./p>
Robert Constable does research on programming languages and formal methods in the context of type theory. The Nuprl proof assistant, developed by Constable and his group, is a dependently-typed language that can be used to describe distributed computing, as a formal specification language for computing tasks, and as a theory for formalizing topics in constructive and intuitionistic mathematics (of which classical mathematics can usually be seen as a special case). Constable is also interested in synthesizing programs and concurrent processes from proofs, developing systems that can be shown to be secure by construction, and exploring the deep connections between programming and logic.
Nate Foster works on language design, semantics, and implementation. In the past, he worked on languages and type systems for data processing, including bidirectional languages and data provenance. More recently, he has been developing the Frenetic language, which provides high-level constructs for specifying the behavior of networks. Frenetic makes it possible for programmers to specify the behavior of an entire network using a single program that a compiler translates to low-level code for the underlying devices. This provides opportunities for enforcing security, reliability, and performance guarantees using language-based techniques.
Dexter Kozen has interests that span a variety of topics at the boundary of computer science and mathematics including the design and analysis of algorithms, computational complexity, decision problems in logic and algebra, and logics and semantics of programming languages. Kozen obtained a number of foundational results for Kleene algebras with tests, and developed applications to efficient code certification and compiler verification. Recently he has been investigating capsules, which provide a clean algebraic representation of state in higher-order functional and imperative languages with mutable bindings, and coalgebraic techniques in verification.
Greg Morrisett focuses on the application of programming language technology for building secure, reliable, and high-performance software systems. A common theme is the focus on systems-level languages and tools that can help detect or prevent common vulnerabilities in software. Past examples include typed assembly language, proof-carrying code, software fault isolation, and control-flow isolation. Recently, his research focuses on building provably correct and secure software, including a focus on cryptographic schemes, machine learning, and compilers.
Andrew Myers works on languages for secure programming, such as Jif, which integrates information flow into Java; Fabric, which extends Jif for building secure distributed systems, and Swift, which automatically partitions web applications securely between the client and the web server. The challenges posed by Fabric and Swift have led to work on language-based methods for controlling timing channels, and on language support for extension and evolution of large software systems, such as the Polyglot extensible Java compiler and the J& language.
Adrian Sampson designs hardware–software abstractions. His work on approximate computing pairs new computer architectures with new programming language constructs to let programmers safely trade off small amounts of accuracy for large returns in efficiency. Challenges in approximate programming range from information-flow control for safety to probabilistic program analysis and compiler design. Sampson is curious about new ways to safely give programmers control over system details that are ordinarily hidden from view.
Fred Schneider has leveraged his research on cyber-security by applying programming logics, semantics, and language design. Recently, he has been working on a "logic of belief" for characterizing authorization policies; this approach is now implemented in the Nexus operating system recently developed here at Cornell. Other examples of his recent work include his hyper-properties characterization of kinds of security policies and his proof that program obfuscation (e.g., address space re-ordering) can be as effective as type checking for defending against cyber-attacks.
Ross Tate works on problems related to language design and formalization including type systems, optimizations, and domain-specific extensions. His work draws on fields such as category theory and constructive type theory to develop powerful and flexible solutions. His research is being put into practice through industry collaborations with Red Hat and JetBrains on the design of the Ceylon and Kotlin languages.