Journal of Symbolic Logic 67 (1):353-368 (2002)
AbstractThe first system of intersection types, Coppo and Dezani , extended simple types to include intersections and added intersection introduction and elimination rules (( $\wedge$ I) and ( $\wedge$ E)) to the type assignment system. The major advantage of these new types was that they were invariant under β-equality, later work by Barendregt, Coppo and Dezani , extended this to include an (η) rule which gave types invariant under βη-reduction. Urzyczyn proved in  that for both these systems it is undecidable whether a given intersection type is empty. Kurata and Takahashi however have shown in  that this emptiness problem is decidable for the sytem including (η), but without ( $\wedge$ I). The aim of this paper is to classify intersection type systems lacking some of ( $\wedge$ I), ( $\wedge$ E) and (η), into equivalence classes according to their strength in typing λ-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
Added to PP
Historical graph of downloads
Similar books and articles
Completeness of the Propositions-as-Types Interpretation of Intuitionistic Logic Into Illative Combinatory Logic.Wil Dekkers, Martin Bunder & Henk Barendregt - 1998 - Journal of Symbolic Logic 63 (3):869-890.
In Quest of 'Good' Medical Classification Systems.Lara K. Kutschenko - 2011 - Medicine Studies 3 (1):53-70.
Classification of Types of Ontogenetic Reproduction.Gavril Acălugăriţei - 1986 - Acta Biotheoretica 35 (1-2):107-121.
A Correspondence Between Martin-Löf Type Theory, the Ramified Theory of Types and Pure Type Systems.Fairouz Kamareddine & Twan Laan - 2001 - Journal of Logic, Language and Information 10 (3):375-402.
Pure Type Systems with More Liberal Rules.Martin Bunder & Wil Dekkers - 2001 - Journal of Symbolic Logic 66 (4):1561-1580.
References found in this work
A New Type Assignment for Λ-Terms.M. Coppo & M. Dezani-Ciancaglini - 1978 - Archive for Mathematical Logic 19 (1):139-156.
Intersection Types for Lambda-Terms and Combinators and Their Logics.Martin Bunder - 2002 - Logic Journal of the IGPL 10 (4):357-378.
Citations of this work
No citations found.