Computing Publications

Publications Home » Cut-Elimination in the Strict Int...

Cut-Elimination in the Strict Intersection Type Assignment System is Strongly Normalising

Steffen van Bakel

Journal Article
Notre Dame Journal of Formal Logic
Volume 45
2004
Abstract

This paper defines reduction on derivations (cut-elimination) in the Strict Intersection Type Assignment System of \cite{Bakel-TCS'92} 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 of terms, using intersection types.

PDF of full publication (203 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.