A bargain for intersection types: A simple strong normalization proof

Abstract

This pearl gives a discount proof of the folklore theorem that every strongly β-normalizing λ-term is typable with an intersection type. (We consider typings that do not use the empty intersection ω which can type any term.) The proof uses the perpetual reduction strategy which finds a longest path. This is a simplification over existing proofs that consider any longest reduction path. The choice of reduction strategy avoids the need for weakening or strengthening of type derivations. The proof becomes a bargain because it works for more intersection type systems, while being simpler than existing proofs. © 2005 Cambridge University Press.