The Lambda Tamer project tackles the issues surrounding computer formalization of programming languages and their metatheories and tools, based around
the Coq proof assistant. The Lambda Tamer methodology centers on
dependently-typed abstract syntax and
denotational semantics. Current outputs include:
- A library with standard formalizations of variable binding, typing contexts, and substitutions
- A generic programming system for automatic generation of common object-language-specific syntactic helper functions and their correctness proofs
- Tactics for automating proofs about code transformations
- A certified type-preserving compiler from lambda calculus to assembly language, implemented in Coq and extractable to OCaml code
