Sciweavers

ENTCS
2002

Strongly Normalising Cut-Elimination with Strict Intersection Types

13 years 9 months ago
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.
Steffen van Bakel
Added 18 Dec 2010
Updated 18 Dec 2010
Type Journal
Year 2002
Where ENTCS
Authors Steffen van Bakel
Comments (0)