1. Hendrik Barendregt (1984): The Lambda Calculus Its Syntax and Semantics, revised edition, Studies in Logic and the Foundations of Mathematics 103. North Holland, doi:10.2307/2274112.
  2. Ernesto Copello: Agda Library for Formal metatheory of the Lambda Calculus using Stoughton's substitution. Available at
  3. Ernesto Copello, Nora Szasz & Álvaro Tasistro (2017): Formal metatheory of the Lambda Calculus using Stoughton's substitution. Theoretical Computer Science 685, pp. 65 – 82, doi:10.1016/j.tcs.2016.08.025.
  4. Martin Copes (2018): A machine checked proof of the Standardization Theorem in Lambda Calculus using multiple substitution. Universidad ORT Uruguay.
  5. H. B. Curry & R. Feys (1958): Combinatory Logic, Volume I. North-Holland. Second printing 1968.
  6. Johannes Emerich & Ignas Vyšniauskas (2014): Coq formalisation of Postponement and Standardization theorems in the untyped lambda-calculus. Available at ILLC, Universiteit van Amsterdam.
  7. Ferruccio Guidi (2012): Standardization and Confluence in Pure Lambda-Calculus Formalized for the Matita Theorem Prover. Journal of Formalized Reasoning 5(1), pp. 1–25, doi:10.6092/issn.1972-5787/3392. Available at
  8. R. Kashima (2000): A Proof of the Standardization Theorem in Lambda-Calculus. Technical Report. Tokyo Institute of Technology. Department of Information Sciences. Available at
  9. James McKinna & Robert Pollack (1999): Some Lambda Calculus and Type Theory Formalized. Journal of Automated Reasoning 23(3), pp. 373–409, doi:10.1023/A:1006294005493.
  10. Ulf Norell (2007): Towards a Practical Programming Language Based on Dependent Type Theory. Department of Computer Science and Engineering, Chalmers University of Technology.
  11. A. Stoughton (1988): Substitution Revisited. Theoretical Computer Science 59, pp. 317–325. Available at
  12. M. Takahashi (1995): Parallel Reductions in λ-Calculus. Information and Computation 118(1), pp. 120 – 127, doi:10.1006/inco.1995.1057. Available at
  13. René Vestergaard & James Brotherston (2003): A Formalised First-Order Confluence Proof for the λ-Calculus using One-Sorted Variable Names. Information and Computation 183(2), pp. 212–244, doi:10.1016/S0890-5401(03)00023-3.

Comments and questions to:
For website issues: