 |
Adam Chlipala Professor of Computer Science Programming Languages & Verification Group (more PL at MIT) Computer Science and Artificial Intelligence Laboratory Department of Electrical Engineering and Computer Science MIT E-mail: adamc@csail.mit.edu Office: 32-G842 |
I'm interested in redeveloping the full stack of tools used by engineers to create hardware-software systems. My traditional areas are programming languages and formal methods (especially with the Coq proof assistant), but I often work on problems at the interfaces with cybersecurity, computer architecture, databases, and operating systems.
When I started as faculty, I didn't know what the heck people meant when asking about my advising style, but now I have some answers. My recruiting these days is mostly focused at the PhD level and below, though I might be persuaded to hire a postdoc with just the right match of expertise. Current MIT students (undergrad, MEng, PhD) interested in working together should e-mail me, while for others I suggest following our normal PhD application process.
For a bit more info on what I work on, two low-time-investment overviews (of the mechanized-proofs part) are my blog post on the surprising security benefits of formal proofs and video of a talk I gave at the 34th Chaos Communication Congress in December 2017.
| End-to-end hardware-software verification | My main interest is in codesigning development tools and system components, across complete digital stacks (hardware and software), for delivering full systems that have unified, machine-checked correctness proofs (usually in Coq). I split my research time about evenly between software and hardware projects, which almost all involve embedding different languages and formal-methods approaches in Coq, with occasional efforts to integrate them together into demos. Our first unified demo was the verified IoT lightbulb, connecting together proofs of a RISC-V microcontroller, the compiler for the Bedrock2 low-level software language, and device drivers and application code written in Bedrock2. Our second unified demo is the verified garage-door opener, which is software-only but includes an implementation of a cryptographic protocol, where most software is generated automatically from functional programs in a variety of ways. The second demo incorporates our Fiat Cryptography project, a domain-specific verified compiler and one of the highest-impact formal-methods projects yet by number of devices that have installed software produced with it (e.g., Fiat Cryptography code ships with essentially all web browsers and mobile platforms in their TLS libraries). |
| End-to-end side-channel security | We are also working toward proofs of timing side-channel security for full hardware-software stacks, tackling both of the main techniques: programming with constant time and using combinations of hardware and software to implement strong process isolation. |
| High-performance computing | I'm ramping up the share of my research attention spent on high-performance computing, broadly construed, including programming with tensors and online transaction processing, with high parallel scaling. I believe multicore hardware architectures as we know them today offer both terrible programming experiences and poor performance scaling, and I'm excited about what comes next, which I'm investigating from the perspectives of both new (verified) software compiler styles and tools for rapid development of new (verified) highly concurrent hardware designs. |
 |
Ur/Web, a domain-specific functional programming language for modern Web applications. I started working on it when I was a grad student, and it's pretty much done research-wise, yielding a production-quality tool suite that a fair number of people enjoy using. |
 |
Lambda Tamer, an umbrella library for the experiments in compiler verification that I started as a grad student. The most concrete outcome of the work was the parametric higher-order abstract syntax (PHOAS) encoding of program syntax, which we still put to use in many of my projects, where different kinds of compilers remain frequent ingredients in novel system designs. |
 |
FSCQ, a file system verified in Coq using a separation logic for reasoning about crash safety, mostly carried out these days by colleagues in the PDOS group |
 |
The Science of Deep Specification, a National Science Foundation Expedition in Computing, 2016-2021, promoting similar full-stack-verification research to what I described above, butf on more conventional architectures |
(An "*" indicates a class I [co]created.)
 |
Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant An introduction to the Coq proof assistant, assuming just familiarity with rigorous math and functional programming. Presents the techniques needed to scale to large formal developments in program verification and other domains, including scripted proof automation and expressive types for embedded programs. |
| FRAP |
Formal Reasoning About Programs Introducing Coq simultaneously with semantics and program proof methods. Emphasizes commonalities through casting (almost) everything in terms of invariants on transition systems, with abstraction and modularity as our standard tools for simplifying invariant proofs. Presents ideas in parallel as chapters of a PDF with standard math notation and in Coq source files, mixing in bits of proof-automation wizardry at the author's whim. [I've used this book so far in six iterations of a graduate class, and I do believe the materials are now ready to be picked up and used pretty directly elsewhere!] |
I'm straying pretty off-topic here, but, especially for all the students who might be reading this far down the page, I'd like to recommend a few books that have had big influences on me and that I wish I'd been told about as a student.
