Abstract

This paper introduces a notion of intersection type assignment on the Lambda Calculus that is a restriction of the BCD-system. This restricted system is essential in the following sense: it is an almost syntax directed system that satisfies all major properties of the BCD-system. The set of typeable terms can be characterized in the same way, the system is complete with respect to the simple type semantics, and it has the principal type property.

Appeared as:

@Inproceedings {Bakel-FSTTCS'93,

Author = "S. van Bakel",
Title = "Essential {I}ntersection {T}ype {A}ssignment",
Booktitle = "Proceedings of FST\&TCS '93. 13$^{\rm th}$ {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience, {\rm Bombay, India}", Editor = "R.K. Shyamasunda",
Series = "Lecture Notes in Computer Science",
Volume = "761",
Publisher = "Springer-Verlag",
Year = "1993",
Pages = "13-23"
}