adam.chlipala.netAdam 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 Contact Information - Publications [ BibTeX ] - CV: HTML , PDF Startup update: Nectry is my startup based on Ur/Web and UPO , with a "no-code" product that sets people across the business world free to build their own "enterprise-software" apps quickly, without knowing a thing about programming. It combines a tasteful component architecture in richly typed functional programming with a large-language-model AI frontend that makes "programming" like chatting with a person who is building your app while you watch. We’re in the earliest stages of setting up pilots with customers, so pointers to potential enthusiastic early adopters are very welcome; and we may be able to hire more engineers soon to do work related to compilers, language design, and IDEs. 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 . Current Research 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. Some Old Research 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 Research Students Postdocs PhD Samuel Gruetter [since Fall 2017] Stella Lau [since Fall 2018] Dustin Jamner [since Fall 2020] Master’s thesis: A Framework for Modular, Extensible, Equivalence-Preserving Compilation Amanda Liu (coadvised with Jonathan Ragan-Kelley ) [since Fall 2020] Master’s thesis: Verified Scheduling Via High-Level Scheduling Rewrites Jiazheng Liu (coadvised with Arvind ) [since Summer 2022] Paul Mure [since Fall 2023] Xin (Amanda) Zhang [since Fall 2023] Master’s Mahmoud Sobier [since Spring 2023] Arthur Reiner De Belen [since Fall 2022] Andrew Tockman [Spring 2021 and since Fall 2023] Julian Zanders [since Fall 2023] Undergraduate Owen Conoly [since Summer 2022] Ritam Nag [since Fall 2022] Leo Gagnon [since Winter 2023] Yue Chen Li [since Winter 2023] Pratyush Venkatakrishnan [Winter-Summer 2023 and since Winter 2024] Chai Lewgasamsarn [since Spring 2023] Sarah Mokhtar Abdella [since Fall 2023] Ali Backour [since Fall 2023] Matthew Habtezgi [since Fall 2023] Michelle Touma [since Fall 2023] Other Past students Teaching Spring 2024: 6.1010: Fundamentals of Programming * (also Fall 2022 , Fall 2021 [as 6.009], Fall 2020 [as 6.009], Spring 2019 [as 6.009], Fall 2017 [as 6.009], Fall 2016 [as 6.009], and Fall 2015 [as 6.S04]) Spring 2023: 6.5120: Formal Reasoning About Programs * (also Spring 2022 [as 6.822], Spring 2021 [as 6.822], Spring 2020 [as 6.822], Spring 2018 [as 6.822], Spring 2017 [as 6.887], and Spring 2016 [as 6.887]) Spring 2015: 6.042: Mathematics for Computer Science (also Spring 2012) Fall 2014: 6.170: Software Studio Fall 2013: 6.820: Foundations of Program Analysis Spring 2013: 6.033: Computer Systems Engineering [recitation instructor] Fall 2012: 6.005: Software Construction Fall 2011: 6.892: Interactive Computer Theorem Proving * (An "*" indicates a class I [co]created.) Books 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...