1 citations · 2 across the 3 of their papers we have counts for
3 papers
cs.LO2026
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…
cs.LO2025★ 1 cited
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.…
cs.LO2023★ 1 cited
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…