Paper Info
Title
A Classification of Intersection Type Systems
Abstract
The first system of intersection types, Coppo and Dezani [3], extended simple types to include intersections and added intersection introduction and elimination rules ((LambdaI) and (LambdaE)) to the type assignment system. The major advantage of these new types was that they were invariant under beta-equality, later work by Barendregt, Coppo and Dezani [11, extended this to include an (eta) rule which gave types invariant under betaeta-reduction. Urzyczyn proved in [6] that for both these systems it is undecidable whether a given intersection type is empty, Kurata and Takahashi however have shown in [51 that this emptiness problem is decidable Cor tire sytem including (eta). but without (LambdaI). The aim of this paper is to classify intersection type systems lacking some of (LambdaI), (LambdaE) and (eta), into equivalence classes according to their strength in typing lambda-terms and also according to their strength in possessing inhabitants. This classification is used in a later paper to extend the above (un)decidability results to two of the five inhabitation-equivalence classes. This later paper also shows that the systems in two more of these classes have decidable inhabitation problems and develops algorithms to find such inhabitants.
Year
DOI
Venue
2002
10.2178/jsl/1190150049
JOURNAL OF SYMBOLIC LOGIC
DocType
Volume
Issue
Journal
67
1
ISSN
Citations 
PageRank 
0022-4812
0
0.34
References 
Authors
8
1
Name
Order
Citations
PageRank
Martin W. Bunder16416.78