Computing Publications

Publications Home » Strongly Normalising Cut-Eliminat...

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
pp.1–18
Elsevier
DOI 10.1016/S1571-0661(04)80488-2
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.

PDF of full publication (266 kilobytes)
(need help viewing PDF files?)
BibTEX file for the publication
N.B.
Conditions for downloading publications from this site.
 

pubs.doc.ic.ac.uk: built & maintained by Ashok Argent-Katwala.