FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Formalization in Constructive Type Theory of the Standardization Theorem

Authors: Martin Copes, Nora Szasz and Alvaro Tasistro

Paper Information

Title:Formalization in Constructive Type Theory of the Standardization Theorem
Authors:Martin Copes, Nora Szasz and Alvaro Tasistro
Proceedings:LFMTP Regular papers
Editors: Giselle Reis and Frédéric Blanqui
Keywords:Formal Metatheory, Lambda Calculus, Constructive Type Theory
Abstract:

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 version 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.

Pages:15
Talk:Jul 07 14:00 (Session 28G: Formalization)
Paper: