2025/03/12 by Barenbaum, Pablo, Della Rocca, Simona Ronchi, Sottile, Cristian
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO)
paper · doi:10.48550/arxiv.2503.09831
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 rely on semantical techniques. In this work, we study Λ_∩e, a variant of Coppo and Dezani's (Curry-style) intersection type system, and we propose a syntactical proof of strong normalization for it. We first design Λ_∩i, a Church-style version, in which terms closely correspond to typing derivations. Then we prove that typability in Λ_∩i implies SN through a measure that, given a term, produces a natural number that decreases along with reduction. Finally, the result is extended to Λ_∩e, since the two systems simulate each other.