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.
Ernesto Copello:
Agda Library for Formal metatheory of the Lambda Calculus using Stoughton's substitution.
Available at https://github.com/ernius/formalmetatheory-stoughton.
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.
Martin Copes (2018):
A machine checked proof of the Standardization Theorem in Lambda Calculus using multiple substitution.
Universidad ORT Uruguay.
H. B. Curry & R. Feys (1958):
Combinatory Logic, Volume I.
North-Holland.
Second printing 1968.
Johannes Emerich & Ignas Vyšniauskas (2014):
Coq formalisation of Postponement and Standardization theorems in the untyped lambda-calculus.
Available at https://github.com/knuton/la-girafe-sportive.
ILLC, Universiteit van Amsterdam.
R. Kashima (2000):
A Proof of the Standardization Theorem in Lambda-Calculus.
Technical Report.
Tokyo Institute of Technology. Department of Information Sciences.
Available at http://www.is.titech.ac.jp/~kashima/pub/C-145.pdf.
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.
Ulf Norell (2007):
Towards a Practical Programming Language Based on Dependent Type Theory.
Department of Computer Science and Engineering, Chalmers University of Technology.
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.