![]() |
Lambda Tamer |
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.
| 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 |