Paper Info
Title
Formalization in Constructive Type Theory of the Standardization Theorem for the Lambda Calculus using Multiple Substitution.
Abstract
We present a full formalization in Martin-Lof'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.
Year
DOI
Venue
2018
10.4204/EPTCS.274.3
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE
Field
DocType
Volume
Discrete mathematics,Lambda calculus,Intuitionistic type theory,sort,Agda,Standardization,Syntax,Structural induction,Calculus,Mathematics
Journal
abs/1807.01871
Issue
ISSN
Citations 
274
2075-2180
0
PageRank 
References 
Authors
0.34
2
3
Name
Order
Citations
PageRank
Martín Copes100.34
Nora Szasz2528.48
Álvaro Tasistro3212.99