Adam Chlipala
Associate 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
Office: 32-G842
Contact Information - Publications [BibTeX] - CV: HTML, PDF
Update on current status: I'm on sabbatical through the end of 2018, splitting my time between normal MIT activities and developing a startup company based on Ur/Web and UPO. Watch this space for a link to the company web site when one exists!

My academic pedigree is in the programming-languages research community, involving such keywords as language design, compilers, program verification, and program derivation. I was lucky enough to start using the Coq proof assistant shortly before mechanized mathematical proofs started to "go mainstream" within the programming-languages community (and, since then, in a few others). Most of my work still involves classic programming-languages aspects, but I've come to view mechanized proofs as another deserving addition to the list that today includes testing, debugging, code review, and version control. That is, they will become a standard tool for everyone developing difficult software or hardware systems. I think of my research agenda as happening to develop foundational proof-assistant tools because most of the rest of the world hasn't realized yet how important they are.

However, today I think of my research interests as covering computer systems broadly construed, including all infrastructure at layers that work with discrete rather than continuous values. A tongue-in-cheek way to put it is (a digital subset of) "the layers that are hard to describe to non-CS friends at parties." In addition to drawing on areas I already mentioned like language design and compilers, my current work touches the traditional areas of computer architecture, cryptography, databases, and operating systems -- where some of the most exciting ideas for me involve making modifications across layers and reconsidering interface boundaries. One recurring theme is using mechanized proofs to move isolation enforcement to compile time. Most of my projects are relevant to security and/or privacy, and I'm also interested in the traditional dimensions of correctness, programmer productivity, and performance.

Interested in joining my research group (at any level: undergrad, masters, PhD, postdoc; already admitted or considering applying)? Please drop me a line to discuss any specific ideas you have for collaboration on projects in programming languages or formal verification!

I've also written a summary of the current "master plan" in the group, which may be useful for people considering applying for student or postdoc positions. Two other low-time-investment overviews 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

Bedrock, a new foundation for an ecosystem of software development tools running entirely inside of Coq, supporting multilanguage programming of systems with assembly-level correctness proofs
Fiat, a Coq framework for refining specifications into efficient programs
FSCQ, a file system verified in Coq using a separation logic for reasoning about crash safety
Kami, a platform for verified hardware programming in Coq
Ur/Web, a domain-specific functional programming language for modern Web applications, inspired by dependent type systems. Supports strong encapsulation of key Web application resources, statically typed metaprogramming, and static analysis for conformance to declarative security policies. Not just a research prototype! Has a growing programmer community and some commercial application development underway.
DeepSpec The Science of Deep Specification, a National Science Foundation Expedition in Computing, 2016-2021

Research Students




Past students


  • Spring 2019: 6.009: Fundamentals of Programming* (also Fall 2017, Fall 2016, and Fall 2015 [as 6.S04])
  • Spring 2018: 6.822: Formal Reasoning About Programs* (also 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.)


    Certified Programming with Dependent Types

    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.


    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 three iterations of a graduate class and plan to fine-tune it through at least one more offering before declaring it beta-quality; but, for intrepid instructors of related classes, it could be worth experimenting with already!]

    Advisory-Board Memberships

  • BedRock Systems [since 2018]: verified systems software for safety-critical computing
  • DARPA Information Science and Technology (ISAT) study group [2018-2021]
  • KryptCo [since 2016]: smarter management for cryptographic keys
  • SiFive [since 2018]: rapid development of custom hardware solutions, based on RISC-V
  • How to Pronounce my Last Name

    Pretend the first "l" isn't there ("Chipala") and you'll get close enough.

    Recommended Reading

    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.

    More content and links....