2 papers
cs.LO2026
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…
cs.LO2026
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…