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

By Kazuhiko Sakaguchi, Nov. 2011 - June 2017.

This is a formalization of the λ-calculus written in SSReflect-Coq and Agda2, and it 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)

References

• 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.