2 citations · 2 across the 4 of their papers we have counts for
4 papers
A formalization of System I with type Top in Agda
Agustín Séttimo, Cristian Sottile, Cecilia Manzino
System I is a recently introduced simply-typed lambda calculus with pairs where isomorphic types are considered equal. In this work we propose a variant of System I with the type T…
Strong normalization through idempotent intersection types: a new syntactical approach
Pablo Barenbaum, Simona Ronchi Della Rocca, Cristian Sottile
It is well-known that intersection type assignment systems can be used to characterize strong normalization (SN). Typical proofs that typable lambda-terms are SN in these systems r…
Two Decreasing Measures for Simply Typed Lambda-Terms (Extended Version)
Pablo Barenbaum, Cristian Sottile
This paper defines two decreasing measures for terms of the simply typed lambda-calculus, called the W-measure and the Tm-measure. A decreasing measure is a function that maps each…
Polymorphic System I
Cristian F. Sottile, Alejandro Díaz-Caro, Pablo E. Martínez López
System I is a simply-typed lambda calculus with pairs, extended with an equational theory obtained from considering the type isomorphisms as equalities. In this work we propose an…