Strong normalization through idempotent intersection types: a new syntactical approach

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