Abstract

This paper defines reduction on derivations in the strict intersection type assignment system of [Bakel-TCS'92], 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.

Key words: intersection types, lambda calculus, termination, cut-elimination.

Appeared as:

@Inproceedings {Bakel-ITRS'02,

Author = "S. van Bakel",
Title = "{S}trongly {N}ormalising {C}ut-{E}limination with {S}trict {I}ntersection {T}ypes",
Series = "Electronic Notes in Theoretical Computer Science",
Volume = "70.1",
Year = "2002",
Note = "http://www.elsevier.nl/locate/entcs/volume70.html" }