Strong normalization through idempotent intersection types: a new syntactical approach

TL;DR

This work studies a variant of Coppo and Dezani's (Curry-style) intersection type system, and proposes a syntactical proof of strong normalization for it, and proves that typability in $Λ_\cap^i$ implies SN through a measure that, given a term, produces a natural number that decreases along with reduction.

Abstract

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 $Λ_\cap^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 $Λ_\cap^i$, a Church-style version, in which terms closely correspond to typing derivations. Then we prove that typability in $Λ_\cap^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 $Λ_\cap^e$, since the two systems simulate each other.