A Formalization of Typed and Untyped λ-Calculi in Coq and Agda2

By Kazuhiko Sakaguchi, Nov. 2011 - July 2020.

This is a formalization of the λ-calculus written in Coq and Agda2, and contains the following definitions and theorems:

SKI combinator calculus: coq/CL.v
- Confluence of weak reduction
Untyped lambda calculus: coq/deBruijn/Untyped.v, agda/Lambda/*.agda
- Confluence of beta reduction
STLC (simply typed lambda calculus): coq/deBruijn/STLC.v
- Subject reduction (type preservation) theorem
- Strong normalization theorem (three different proofs are available)
System F (second order typed lambda calculus): coq/deBruijn/F.v
- Subject reduction (type preservation) theorem
- Strong normalization theorem (three different proofs are available)

Useful Literature

T. Altenkirch. A Formalization of the Strong Normalization Proof for System F in LEGO. Typed Lambda Calculi and Applications, 13-28, 1993.
N.G. de Bruijn. Lambda Calculus Notation with Nameless Dummies: A Tool for Automatic Formula Manipulation, with Application to the Church-Rosser Theorem. Indagationes Mathematicae, 75(5), 381–392, 1972.
J.H. Gallier. On Girard's “Candidats de Réductibilité". In Logic and Computer Science. P. Odifreddi, Editor, Academic Press, 123-203, 1989.
J.-Y. Girard. Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur. Thèse d'état, Université de Paris 7. 1972.
J.-Y. Girard, Y. Lafont and P. Taylor. Proofs and Types. Cambridge University Press, 1989.
J.R. Hindley and J.P. Seldin. Lambda-Calculus and Combinators: an Introduction. Cambridge University Press, 2008. 3rd edition.
C.-K. Hur. Heq : a Coq library for Heterogeneous Equality. http://sf.snu.ac.kr/gil.hur/Heq/
T. Nipkow. More Church-Rosser Proofs (in Isabelle/HOL). Journal of Automated Reasoning, 26(1), 51–66, 2001.
A. Popescu, C.J. Osborn and E.L. Gunter. Strong Normalization for System F by HOAS on Top of FOAS. Logic in Computer Science, 31-40, 2010.
M. Takahashi. Parallel Reductions in λ-Calculus. Information and Computation, 118(1), 120-127, 1995.
大堀淳. プログラミング言語の基礎理論, 情報数学講座, 第9巻, 共立出版, 1997.
横内寛文. プログラム意味論, 情報数学講座, 第7巻, 共立出版, 1994.