A Formalization of Typed and Untyped λ-Calculi in SSReflect-Coq and Agda2
Coq Agda Other
Switch branches/tags
Nothing to show
Clone or download
Latest commit c71454c Dec 18, 2017
Permalink
Failed to load latest commit information.
agda/Lambda refactoring Jan 9, 2012
coq small cleanup Dec 18, 2017
.gitignore small cleanup Dec 18, 2017
README.ja.mkd small cleanup Dec 18, 2017
README.mkd small cleanup Dec 18, 2017
build small cleanup Dec 18, 2017
config.el Start to formalizing the Girard's SN proof. Aug 2, 2014

README.mkd

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.