Lambda-Calculi-Coq

Lambda-Calculi implementations & proofs in Coq.

Features:

• Church-Rossner Confluence of beta-reductions for the untyped lambda calculus.
• Progress, preservation, & strong-normalization of the simply-typed lambda calculus.
• Preservation & progress of System F.

Sources

I borrow heavily from the following for coq-certified de Bruijn notation calculi. Many techniques & lemmas I employ are not of my own design, & these repositories are my reference.

• Coq-In-Coq

• Lambda-Calculus

• PLFA

For general wisdom on coq-programming I looked to:

• Software Foundations

• Certified Programming with Dependent Types

And of course, Types and Programming Languages is an important source.