Programming Languages

The programming languages research group at Cornell includes eight faculty and over two 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.

See the PL group's site for news and a full list of people involved in PL research.

Faculty

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.

Justin Hsu designs methods to formally verify that programs are correct, especially programs that use randomization. His research blends ideas from two classical areas of computer science: randomized algorithms from theoretical computer science (TCS) and formal verification. In the past, a particular focus of his work has been differential privacy, a rigorous definition of privacy that is currently under extensive study. He have investigated a variety of formal methods—such as type systems and program logics—to verify that programs are differentially private. More broadly, he is interested in developing programming languages and formal verification methods for quantiatitve properties and quantitative programs, including algorithms from security, machine learning, and economics.

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 designs and extends languages to solving cross-cutting problems such as computer security.  The Jif language integrates information flow control into Java, and Fabric extends Jif for building secure, decentralized distributed systems. Follow-on work includes language-based methods for controlling timing channels at the software and hardware levels: the SecVerilog hardware description language used to design the HyperFlow processor, the Viaduct project which compiles high-level code to cryptography, and applications to blockchains and smart contracts. These projects have also motivated work on language support for debugging, extending, and evolving large software systems, including the Genus and Familia languages and the SHErrLoc error localizer.

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.

Alexandra Silva does research in programming language semantics, automata, and verification. Much of her work is developed from the unifying perspective offered by coalgebra, a mathematical framework established in the last decades. In the last years, Alexandra's work focussed on probabilistic languages, concurrency and Kleene algebra, and the use of automata learning in verification. 

Emeritus

Robert Constable researches 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.