Adam Chlipala
E-mail: adam@chlipala.net

I finished my PhD in Computer Science at Berkeley in 2007. I received a Master of Science degree in CS from Berkeley in 2004 and a Bachelor of Science in CS from CMU in 2003.

I'm currently doing a part-time postdoc with Greg Morrisett at Harvard. In the other half of my time, I'm working on a stealth-mode Internet start-up company built around type theory.

One of my primary research interests is engineering issues in interactive computer theorem proving, especially as related to the formal semantics of programming languages. Over the years, software developers have settled upon techniques that promote long-term maintainability of software. The field of mechanized theorem-proving sorely lacks its own counterpart. Most mechanized proofs are hard to write, understand, and evolve. We should be writing our machine-checked proofs in a way that makes them easy to adapt to changing specifications, following a standard lesson of software development. My research on computer theorem proving focuses on techniques for rapid construction of readable, automated proofs (especially in Coq), without giving up the expressivity of higher-order logic.

I'm also interested in the design and implementation of statically-typed functional programming languages, especially those with interesting facilities for type-level computation. I'm working on the Ur/Web programming language and compiler, which make it possible to generate large parts of dynamic web applications with statically-typed metaprogramming.

Certified Compilers Now!

Starting with my thesis research, I've been developing the Lambda Tamer library for programming language formalization in Coq. I'm working towards a certified compiler for core ML; that is, a compiler with a machine-checked proof that it preserves program meanings. I follow a somewhat unusual style, including a few key elements:

  1. Using dependently-typed abstract syntax to combine syntax with typing rules, so that program transformations can be verified as type-preserving through simple type checking
  2. Formalizing abstract syntax using a new technique called parametric higher-order abstract syntax, which represents object language variable binders with meta language binders, while still making it possible to write a variety of useful recursive, pattern-matching functions over syntax
  3. For strongly-normalizing languages, using foundational type-theoretic semantics instead of the more popular operational semantics, so that formalized object languages can inherit almost all of their dynamic semantics from Coq's Calculus of Inductive Constructions
  4. For Turing-complete languages, using substitution-free operational semantics to delegate implementation of substitution to the meta language
  5. Performing semantic preservation proofs with aggressive theorem-specific proof automation via Coq's Turing-complete Ltac language

Papers:

  1. Syntactic Proofs of Compositional Compiler Correctness, submitted draft
  2. A Verified Compiler for an Impure Functional Language, POPL'10
  3. Parametric Higher-Order Abstract Syntax for Mechanized Semantics, ICFP'08
  4. A Certified Type-Preserving Compiler from Lambda Calculus to Assembly Language, PLDI'07

Certified Programming with Dependent Types textbook

I'm writing a textbook on effective engineering with Coq. It's reached a stable state that I'm calling a complete beta release.

This book should be valuable even to most people who have been using Coq for years, since 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.

Ur/Web: Statically-typed metaprogramming for the web

I'm working on a new breed of domain-specific programming language for database-backed web applications. The static type system rules out code-injection attacks and many common kinds of web programmer negligence. Beyond that, I've added features from the world of dependent types, especially to support metaprogramming, where programs can be written by recursion on type structure. This makes it possible to reify as well-typed functions many "design patterns" that show up via copy-and-paste in most of today's web applications.

Papers:

  1. Ur: Statically-Typed Metaprogramming with Type-Level Record Computation, PLDI'10

Ynot: Imperative programming for Coq

The Ynot library turns Coq into an environment for writing and verifying imperative programs. We support compilation to native code via extraction to OCaml, and there are goodies for automating large parts of most proofs about heaps and data structures.

Papers:

  1. Effective Interactive Proofs for Higher-Order Imperative Programs, ICFP'09

Other Research

The Standard Stuff

Software

...and All the Rest