79 citations
- Universidad de la República de UruguayUY24 papers
- Universidad Politécnica de MadridES6 papers
- Johns Hopkins UniversityUS2 papers
- Universidad de MontevideoUY2 papers
- Universidade de São PauloBR2 papers
- Universidad Nacional de CórdobaAR2 papers
- Airbus (Germany)DE1 paper
- Association Clinique et Thérapeutique Infantile du Val de MarneFR1 paper
- California Institute of TechnologyUS1 paper
- Carnegie Mellon UniversityUS1 paper
- Centre National de la Recherche ScientifiqueFR1 paper
- Consejo de Formación en EducaciónUY1 paper
6 papers · 1 filter
A Machine-checked Proof of Consistency for Impredicative Pure Type Systems
Sebastián Urciuoli
In this paper we continue assessing the feasibility of the approach to the mechanization of type theory by using classical syntax and Stoughton's multiple substitutions and report…
Dependently Sorted Nominal Signatures
Maribel Fernández, Miguel Pagano, Nora Szasz +1
We investigate an extension of nominal many-sorted signatures in which abstraction has a form of instantiation, called generalised concretion, as elimination operator (similarly to…
On the Formal Metatheory of the Pure Type Systems using One-sorted Variable Names and Multiple Substitutions
Sebastián Urciuoli
We develop formal theories of conversion for Church-style lambda-terms with Pi-types in first-order syntax using one-sorted variables names and Stoughton's multiple substitutions.…
A Formal Proof of the Strong Normalization Theorem for System T in Agda
Sebastián Urciuoli
We present a framework for the formal meta-theory of lambda calculi in first-order syntax, with two sorts of names, one to represent both free and bound variables, and the other fo…
Nominal Sets in Agda -- A Fresh and Immature Mechanization
Miguel Pagano, José E. Solsona
In this paper we present our current development on a new formalization of nominal sets in Agda. Our first motivation in having another formalization was to understand better nomin…
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…