Programming Languages at Harvard
The Programming Languages Group is composed of faculty and students (in MD309)
at the School of Engineering and Applied
Sciences who are interested in problems relating to programming language
foundations, design, and implementation.
The PL Seminar typically happens Wednesdays at 1600 in Maxwell Dworkin 223. We
occasionally have speakers at other times. Check the PL Seminar's
The CertiCoq project aims to build a proven-correct compiler for
dependently-typed, functional languages, such as Gallina—the core
language of the Coq proof assistant. A proven-correct compiler consists of a
high-level functional specification, machine-verified proofs of important
properties, such as safety and correctness, and a mechanism to transport
those proofs to the generated machine code. The project exposes both
engineering challenges and foundational questions about compilers for
- Shill: Scripting with Least Privilege
Shill is a shell scripting language designed to make it easy to follow the
Principle of Least Privilege. Shill uses capabilities to control what access
scripts have to your system. Every Shill script comes with a contract that
describes what it can do, so users can run third-party scripts with
confidence. Using capability-based sandboxes, Shill's security guarantees extend
even to native executables launched by scripts.
- GoNative: Safe Execution of Native Code
The goal of the GoNative research project is to enable safe execution of
native code in software systems such as web browsers and type-safe
programming languages (e.g., Java, Python, C#).
The Accrue project aims to provide language-based information security
guarantees that are proportional to programmer effort. With little effort, a
programmer may receive only weak (but, ideally, formal) guarantees; with
more effort, a programmer should receive stronger guarantees. The Accrue
project enables inference and discovery of strong information security
guarantees in Java programs.
- Privacy Tools for Sharing Research Data
We have two mailing lists dedicated to programming
languages. The md309
list is for students and former students of the PL
Lab. The programming
list is for a wider audience of people (at Harvard and elsewhere) who are
interested in programming languages.
Recent Ph.D. Alumni
Recent Post-doc Alumni