"Computer scientists, as all scientists, seek a common framework in which to link and organize many levels of explanation; moreover, this common framework must be semantic, since our explanations (including programs) are typically in formal language." --Robin Milner

From the beginning, Cornell has been known for its research in programming languages, which spans everything from logics and language semantics to language design, optimizing compilers, and software engineering. We are proud of both our breadth and depth in this core discipline. Programming Languages is a lively area at Cornell with at least five faculty and over 20 Ph.D. students.

Examples of our research in programming languages include the foundational work of Robert Constable on type theory and automated theorem proving. However, our strength lies not only in the theory of programming languages, but also practical issues such as their implementation.

The Language-Based Security project, involving faculty members Fred Schneider, Dexter Kozen, and Andrew Myers, studies new security enforcement mechanisms based on program analysis and transformation. Advanced type systems are used to ensure certifiable security properties; programs are transformed to remove security vulnerabilities. This new approach to computer security is well suited to networked computing systems built from extensible and mobile components.

The goal of the ISS research group is to build intelligent software systems for automatically enhancing the efficiency and survivability of programs, thereby enabling applications programmers to focus on high-level algorithmic issues. Current work includes self-optimizing high-performance library generation, automatic application-level fault tolerance, and web services for grid computing.

There is much synergy between researchers in programming languages and logic and other research areas. For example, the Nuprl group works closely with Ken Birman and the Ensemble group to verify the correctness of the Ensemble group communication system written in ML. The work on language-based security also spans the areas of computer security, systems, and programming languages.

Faculty and Researchers

Robert Constable
Dexter Kozen
Andrew C. Myers
Keshav Pingali
Radu Rugina
Fred B. Schneider
Tim Teitelbaum
Christoph Kreitz

Ongoing and Recent Projects

NuPRL
Jif
Jx/J&
JMatch
Polyglot
Crystal
SATC
Frex
ECC
KAT
ISS