Strong normalization through idempotent intersection types: a new syntactical approach

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