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. 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. Performing semantic preservation proofs using proof by decision procedure, where manual specification of the details of proofs is avoided in favor of writing custom proof-producing decision procedures in Coq's Turing-complete Ltac language

Relevant recent papers:

1. Parametric Higher-Order Abstract Syntax for Mechanized Semantics, ICFP'08
2. A Certified Type-Preserving Compiler from Lambda Calculus to Assembly Language, PLDI'07

Other Research

• Certified program verifiers
• Proof-carrying code
• Tool support for interactive computer theorem proving
• Program analysis
• Software model checking
• Typed compiler intermediate languages

The Standard Stuff

• My publications
• As BibTeX
• My CV
• In PostScript
• In PDF
• Resumé, for jobs outside computer science research (PDF)
• LinkedIn profile

Software

• Cooperative Internet hosting tools, including DomTool, a domain-specific language in support of shared UNIX system configuration by mutually-untrusting users
• Laconic/Web, a prototype domain-specific programming language design and implementation supporting meta-programming of web applications with strong static guarantees
• Dynamic web site tools for Standard ML, including separately usable libraries for accessing SQL databases
• Links to sundry other projects can be found from my SourceForge profile.
• Most of this web site is built from an XML database using XSLT. I've published my code for doing this.

...and All the Rest

• Course on Interactive Computer Theorem Proving (focusing on Coq) that I taught in Fall 2006
• A point-by-point comparison of the Objective Caml and Standard ML programming languages
• Challenge problems and solutions that I've posted on the POPLmark mailing list
• Looking for Internet hosting where you can go wild developing Internet services with your favorite non-mainstream programming language? Join HCoop, the Internet Hosting Cooperative!
• My personal web site
• Archival version of my last web site at Berkeley
• Best upper bound on my Erdös Number that I know of: 4