This paper defines reduction on derivations in the strict intersection type assignment system of  by generalising cut-elimination, 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. © 2003 Published by Elsevier Science B.V.
Van Bakel, S. (2003). Strongly normalising cut-elimination with strict intersection types. In Electronic Notes in Theoretical Computer Science (Vol. 70, pp. 21–38). https://doi.org/10.1016/S1571-0661(04)80488-2