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

TL;DR

This paper provides a fully formalized proof of the Standardization Theorem for the Lambda Calculus within Constructive Type Theory, utilizing multiple substitution and machine-checked in Agda, ensuring rigorous correctness.

Contribution

It introduces a formalization of the Standardization Theorem using first-order syntax and multiple substitution within Constructive Type Theory, verified by machine proof in Agda.

Findings

Formal proof of the Standardization Theorem in Agda

Use of multiple substitution with first-order syntax

Proof based on structural induction over syntax

Abstract

We present a full formalization in Martin-L\"of'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.