Home

Awesome

Iron Lambda

Iron Lambda is a collection of Coq formalizations for functional languages of increasing complexity. All proofs use straight deBruijn indices for binders.


Proofs that are "done" have at least Progress and Preservation theorems.