Lambda Tamer old releases

20091030 release of the Lambda Tamer library

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

20090926 release

This release centers on the Compose example, which shows how to verify a CPS translation such that the resulting code can be linked soundly with code produced by different compilers.

20090710 release

This release centers on the Untyped example, which is a verified compiler to an idealized assembly language from an untyped Mini-ML language. The universal operational semantics from the last release is replaced by the more standard one-operational-semantics-per-language.

20080620 release

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.