Lambda Tamer

The Lambda Tamer project tackles the issues surrounding computer formalization of programming languages and their tools, based around the Coq proof assistant. The Lambda Tamer methodology centers on higher-order and dependently-typed abstract syntax and aggressive automation. The main project output is a library of Coq definitions, theorems, and tactics in support of building certified compilers for HOT (higher-order typed) languages.

New: 20091106 release of the Lambda Tamer library

This is the final release to go with the POPL'10 paper, focusing on the verified compiler from an impure Mini-ML language to an idealized assembly language.

Warning: This is the first release meant to work with Coq 8.2. Only the more recent examples (Untyped and Compose) have been verified to compile with 8.2.

Some old releases are still available.

Papers

Composable theorems	Syntactic Proofs of Compositional Compiler Correctness	submitted draft
Impure languages	A Verified Compiler for an Impure Functional Language	POPL'10
Syntax & pure languages	Parametric Higher-Order Abstract Syntax for Mechanized Semantics	ICFP'08
Mostly-superceded initial work	A Certified Type-Preserving Compiler from Lambda Calculus to Assembly Language	PLDI'07

Author: Adam Chlipala

Project summary page