Theoretical Pearls: A bargain for intersection types: a simple strong normalization proof

Abstract

This pearl gives a discount proof of the folklore theorem that every strongly 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.