Adam Chlipala
Associate Professor without Tenure 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
The basic mission of my research group is to build the programming platform of the future, based on close integration of computer theorem-proving tools, especially the Coq proof assistant. While formal methods are commonly viewed today as an extra (and non-cost-effective!) activity piled on top of the normal programming process, I believe that machine-checked proofs will have a transformative effect on the development process by enabling new forms of abstraction and modularity, with associated benefits in lowered human effort and improved security and performance. We are gradually piecing together a proof-of-concept platform that runs inside of Coq, where the theorem prover becomes the IDE that the programmer interacts with primarily from the beginning of a project. Ongoing work considers different abstraction levels, including mathematical specifications, functional programs, imperative programs, assembly language, and circuits suitable to be turned into hardware. A running theme throughout the different layers is highly automated formal proofs that still prove deep theorems from first principles. We also use functional programming with rich type systems almost everywhere.

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.

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

Postdocs

PhD

Master's

Undergraduate

Other

Past students

Teaching

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

    • Books

    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.
    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 two 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!]

    How to Pronounce my Last Name

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