2 papers
cs.LO2018
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…
cs.PL2018
Formalisation in Constructive Type Theory of Barendregt's Variable Convention for Generic Structures with Binders
Ernesto Copello, Nora Szasz, Álvaro Tasistro
We introduce a universe of regular datatypes with variable binding information, for which we define generic formation and elimination (i.e. induction /recursion) operators. We then…