activity
20152025
most citedFormalisation in Constructive Type Theory of Barendregt's Variable Convention for Generic Structures with Binders

6 citations · 9 across the 5 of their papers we have counts for

collaborators
Showing 2018Show all

2 papers · 1 filter

cs.LO2018★ 3 cited

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★ 6 cited

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…