Formalization in Constructive Type Theory of the Standardization Theorem for the Lambda Calculus using Multiple Substitution

Martín Copes
Nora Szasz
(Universidad ORT Uruguay)
Álvaro Tasistro
(Universidad ORT Uruguay)

We present a full formalization in Martin-Löf's Constructive Type Theory of the Standardization Theorem for the Lambda Calculus using first-order syntax with one sort of names for both free and bound variables and Stoughton's multiple substitution. Our formalization is based on a proof by Ryo Kashima, in which a notion of beta-reducibility with a standard sequence is captured by an inductive relation. The proof uses only structural induction over the syntax and the relations defined, which is possible due to the specific formulation of substitution that we employ. The whole development has been machine-checked using the system Agda.

In Frédéric Blanqui and Giselle Reis: Proceedings of the 13th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2018), Oxford, UK, 7th July 2018, Electronic Proceedings in Theoretical Computer Science 274, pp. 27–41.
Published: 3rd July 2018.

ArXived at: http://dx.doi.org/10.4204/EPTCS.274.3 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org