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.
Mendeley saves you time finding and organizing research
Choose a citation style from the tabs below