Adam Chlipala
Assistant Professor of Electrical Engineering and Computer Science
Douglas T. Ross (1954) Career Development Professor of Software Technology
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
My research applies formal logic to improve the software development process. I spend a lot of time proving programs correct with the Coq computer proof assistant, with a focus on reducing the human cost of program verification so that we can imagine that it could one day become a standard part of software development (at least for systems software). I'm also interested in the design and implementation of programming languages, especially functional or otherwise declarative languages, especially when expressive type systems (particularly dependent type systems) are involved. I usually stick to very low-level or very high-level languages; I believe that most "general-purpose languages" of today fail to hit the mark by being, for any particular software project, either too low-level or too high-level.

I'm just getting started at MIT and looking to get some fun projects rolling. 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 my research interests and projects, which may be useful for people considering applying for student or postdoc positions.

Current Research

Bedrock, a new low-level programming language, embedded within Coq, with support for mostly-automated verification of functional correctness. My goal is to use Bedrock to implement a complete verified software stack that can rely on static verification to take over from uses of dynamic techniques for enforcing process isolation.
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.

Research Students

Postdocs

PhD

Master's

Undergraduate

Other

Past students

Teaching

  • Spring 2013: 6.033: Computer Systems Engineering [recitation instructor]
  • Fall 2012: 6.005: Software Construction
  • Spring 2012: 6.042: Mathematics for Computer Science
  • Fall 2011: 6.892: Interactive Computer Theorem Proving

    • An In-Progress Textbook

    Certified Programming with Dependent Types is a pragmatic introduction to the Coq computer proof assistant. I focus on a very unusual approach, centered on replacing manual proofs with lots of dependent types and mostly automated proofs based on scripted decision procedures.

    How to Pronounce my Last Name

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