Strongly Normalising Cut-Elimination with Strict Intersection Types

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

• Type: Journal
• Year: 2002
• Where: ENTCS
• Authors: Steffen van Bakel
• Keywords: ENTCS 2002, Intersection Type Assignment, Intersection Types, Key Words