坂口和彦 2011/11-2017/6
現時点でこの形式化は、以下の定義と定理を含んでいる。
- SKIコンビネータ計算: coq/CL.v
- weak reduction の合流性
- 型無しλ計算: coq/deBruijn/Untyped.v, agda/Lambda/*.agda
- beta reduction の合流性
- 単純型付きλ計算: coq/deBruijn/STLC.v
- 主部簡約(型保存)定理
- 強正規化定理(3通りの異なる方法で証明)
- System F (二階型付きλ計算): coq/deBruijn/F.v
- 主部簡約(型保存)定理
- 強正規化定理(3通りの異なる方法で証明)
- 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.