Strongly Normalising Cut-Elimination with Strict Intersection Types
Steffen van Bakel · Electronic Notes in Theoretical Computer Science · 2003
This paper defines reduction on derivations in the strict intersection type assignment system of [2], by generalising cutelimination, and shows a strong normalisation result for this reduction. Using this result, new proofs are given for the approximation theorem and the characterisation of normalisability using intersection types.