Abstract

This paper defines reduction on derivations (cut-elimination) in the Strict Intersection Type Assignment System of \cite{Bakel-TCS'92} 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 of terms, using intersection types.

Appeared as:

@Article{Bakel-NDJFL'04,

Author = "S. van Bakel",
Title = "Cut-{E}limination in the {S}trict {I}ntersection {T}ype {A}ssignment {S}ystem is {S}trongly {N}ormalising.",
Year = "2004",
Journal = "Notre Dame journal of Formal Logic",
Volume = "45",
Number = "1"
}