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.
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.
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.
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.
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.