"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 five faculty and over a dozen Ph.D. students.

Our strength lies not only in the theory of programming languages, but also practical issues such as their implementation. The foundational work of Robert Constable on type theory and automated theorem proving, and the work of Andrew Myers, Dexter Kozen, and Fred Schneider on language-based security, exemplify Cornell's range.

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.

Faculty and Researchers

Robert Constable
Dexter Kozen
Andrew C. Myers
Fred B. Schneider
Tim Teitelbaum

Ongoing and Recent Projects

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