Lambda Tamer

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:

Source Distributions

From the SourceForge download page, you can obtain:


Documentation on installation and implementation

A quick example: A certified CPS translation for simply-typed lambda calculus


Author: Adam Chlipala

Project summary page

SourceForge Logo