We give Coq formalizations of two proofs showing well-known results about the untyped lambda calculus.
The main results are complete proofs of the Postponement and Standardization theorems, formalizing parts of, respectively:
- Masako Takahashi.
Parallel Reductions in Lambda-calculus
(Information and Computation, Volume 118, 1995) - Ryo Kashima.
A Proof of the Standardization Theorem in Lambda-Calculus
Research Reports on Mathematical and Computing Sciences, C-145, (Tokyo Institute of Technology, 2000).
This work was done as a study project by Ignas Vyšniauskas (@yfyf) and Johannes Emerich (@knuton).
