Strongly Normalising Cut-Elimination with Strict Intersection Types
Steffen van Bakel
- Conference or Workshop Paper
- 2nd International Workshop on Intersection Types and Related Systems (ITRS'02), Copenhagen, Denmark
- July, 2002
- Electronic Notes in Theoretical Computer Science
- Volume 70
- Issue 1
- DOI 10.1016/S1571-0661(04)80488-2
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.
- PDF of full publication (266 kilobytes)
- (need help viewing PDF files?)
- BibTEX file for the publication
- Conditions for downloading publications from this site.