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 dependently-typed abstract syntax and foundational type-theoretic semantics. 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: 20080620 release of the Lambda Tamer library

Adds support for formalizing impure object languages and their transformations, via a deep embedding of a meta language with opt-in dynamic typing. The big case study is a CPS translation for an idealized version of monomorphic core ML.

20080328 release

This release goes with the ICFP'08 paper, and later releases supercede it. It's a complete reimplementation based on a new syntax encoding technique, parametric higher-order abstract syntax, in place of de Bruijn indices. This release also doesn't include any OCaml code for Coq plug-ins, so it should work with Coq 8.1+, in contrast to the previous release. Examples in the distribution include CPS translation and closure conversion for simply-typed lambda calculus, CPS translation for System F, and a pattern match compiler.

The initial Lambda Tamer release is still available. See the old front page.

Papers

Syntax	Parametric Higher-Order Abstract Syntax for Mechanized Semantics	ICFP'08
Semantics	Report on foundational type-theoretic semantics for higher-order, impure object languages coming soon....
Mostly-superceded initial work	A Certified Type-Preserving Compiler from Lambda Calculus to Assembly Language	PLDI'07