 |
Adam Chlipala Arthur J. Conner (1888) 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: [email protected] Office: 32-G842 |
My traditional research-area home is the intersection of programming languages and formal methods (especially with the Coq proof assistant). Most projects I do involve compilers that are proved in some way or another. Early in my time at MIT, I also picked up an interest in digital hardware designs (and the tools for writing, verifying, and compiling them), which makes up about half of my research today.
My first run of years as faculty was focused on deriving the highest formal assurance of correctness and security for digital systems. In service of completeness of formal reasoning, it was often convenient to choose relatively simple but important code bases. A good example would be a critical piece of library code, whose verified compilation we supported in the Fiat Cryptography project, producing intricate cryptographic arithmetic code today included in the TLS libraries of all major web browsers. Another favorite strategy was focusing on embedded systems, including theorems spanning hardware and software (as in our verified IoT lightbulb) and end-to-end proof of a bare-metal software image for a cryptographic server (as in our verified garage-door opener).
I'm trying to focus lately on the full stack of high-performance parallel computing: software and hardware, language design, compilers, and verification tools. Partly this choice comes from wanting to do formal methods on the most impactful kinds of systems. However, I also think the experience of developing high-performance code has stagnated, in a way that industry is unlikely to escape from on its own. My cheeky summary of the problem is that "assembly language is over," basically suggesting that a lowest-level software language will fail to serve us well in the near future if it (1) is inherently sequential (one instruction after another) or (2) hides data movement (through caching systems for memory). We should be able to do a lot better by rethinking abstractions and tools, along the whole path from very high-level languages (perhaps even high-level enough to say they are for "specifications") to gate-level hardware designs. I want to build unified machine-checked proofs that span this whole gap, while also innovating in all of the layers involved. So, I'm especially glad to recruit students who, ideally, have strong experience implementing and debugging compilers and low-level software/hardware systems, as well as carrying out machine-checked proofs of significant artifacts!
The specific shape of this work today is clustered roughly around: (1) unified languages for building highly parallel systems that are at least "hardware-style," with modular verification tools and verified compilation; and (2) verified compilers translating more "software-style" programs to run on such substrates, where those source programs take advantage of nice programming abstractions, certainly with nothing as grungy as ad-hoc use of locks to protect shared memory. I hope these lines of work eventually merge together, through identifying good shared intermediate languages for compiling software, hardware, and the interface between them.
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. (I won't usually agree to an ad-hoc interview call with a candidate not yet at MIT, since evidence from social science indicates interviews decrease decision quality by promoting irrational bias.)
(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.