Computing Publications

Publications Home » Complete restrictions of the Inte...

Complete restrictions of the Intersection Type Discipline

Steffen van Bakel

Journal Article
Theoretical Computer Science
Volume 102
Issue 1
pp.135–163
August, 1992
Elsevier
DOI 10.1016/0304-3975(92)90297-S
Abstract

In this paper the BCD intersection type discipline is studied. We will present two different and independent complete restrictions of the intersection type discipline. The first restricted system, the strict type assignment system, is presented in section two. Its major feature is the absence of the derivation rule (<=) and it is based on a set of strict types. We will show that these together give rise to a strict filter lambda model that is essentially different from the one presented in BCD'83. We will show that the strict type assignment system is the nucleus of the full system, i.e. for every derivation in the intersection type discipline there is a derivation in which (<=) is used only at the very end. Finally we will prove that strict type assignment is complete for inference semantics. The second restricted system is presented in section three. Its major feature is the absence of the type omega. We will show that this system gives rise to a filter lambda I-model and that type assignment without omega is complete for the lambda I-calculus. Finally we will prove that a lambda term is typeable in this system if and only if it is strongly normalizable.

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