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

Autor:	Copes, Martín, Szasz, Nora, Tasistro, Álvaro
Rok vydání:	2018
Předmět:	Computer Science - Logic in Computer Science
Zdroj:	EPTCS 274, 2018, pp. 27-41
Druh dokumentu:	Working Paper
DOI:	10.4204/EPTCS.274.3
Popis:	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. Comment: In Proceedings LFMTP 2018, arXiv:1807.01352
Databáze:	arXiv
Externí odkaz:	http://arxiv.org/abs/1807.01871 Zobrazit plný text záznamu View this record from Arxiv