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

Martín Copes, Nora Szasz, Álvaro Tasistro

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…