Cut-Elimination in the Strict Intersection Type Assignment System is Strongly Normalizing
Steffen van Bakel · Notre Dame Journal of Formal Logic · 2004
This paper defines reduction on derivations (cut-elimination) in the Strict Intersection Type Assignment System of an earlier paper and shows a strong normalization result for this reduction. Using this result, new proofs are given for the approximation theorem and the characterization of normalizability of terms using intersection types.