Formalization in Constructive Type Theory of the Standardization Theorem for the Lambda Calculus using Multiple Substitution
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 both free and bound variables and Stoughton's multiple substitution. Our formalization is based on a proof by...
Main Authors: | Martín Copes, Nora Szasz, Álvaro Tasistro |
---|---|
Format: | Article |
Language: | English |
Published: |
Open Publishing Association
2018-07-01
|
Series: | Electronic Proceedings in Theoretical Computer Science |
Online Access: | http://arxiv.org/pdf/1807.01871v1 |
Similar Items
-
Standardization and Confluence in Pure Lambda-Calculus Formalized for the Matita Theorem Prover
by: Ferruccio Guidi
Published: (2012-01-01) -
Standardization in resource lambda-calculus
by: Maurizio Dominici, et al.
Published: (2012-11-01) -
Formalisation in Constructive Type Theory of Barendregt's Variable Convention for Generic Structures with Binders
by: Ernesto Copello, et al.
Published: (2018-07-01) -
Fundamental theorems of extensional untyped $\lambda$-calculus revisited
by: Alexandre Lyaletsky
Published: (2015-10-01) -
Models and theories of lambda calculus
by: Manzonetto, Giulio
Published: (2008)