David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Jack Alan Reynolds
Learn more about PhilPapers
Journal of Symbolic Logic 67 (1):353-368 (2002)
The 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
|Keywords||No keywords specified (fix it)|
|Categories||categorize this paper)|
Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
|Through your library|
References found in this work BETA
No references found.
Citations of this work BETA
No citations found.
Similar books and articles
Wil Dekkers, Martin Bunder & Henk Barendregt (1998). Completeness of the Propositions-as-Types Interpretation of Intuitionistic Logic Into Illative Combinatory Logic. Journal of Symbolic Logic 63 (3):869-890.
Martin Bunder & Wil Dekkers (2001). Pure Type Systems with More Liberal Rules. Journal of Symbolic Logic 66 (4):1561-1580.
Fairouz Kamareddine & Twan Laan (2001). A Correspondence Between Martin-Löf Type Theory, the Ramified Theory of Types and Pure Type Systems. Journal of Logic, Language and Information 10 (3):375-402.
Gavril Acălugăriţei (1986). Classification of Types of Ontogenetic Reproduction. Acta Biotheoretica 35 (1-2):107-121.
Lara Kutschenko (2011). In Quest of 'Good' Medical Classification Systems. Medicine Studies 3 (1):53-70.
Wayne Aitken & Jeffrey A. Barrett (2007). Stability and Paradox in Algorithmic Logic. Journal of Philosophical Logic 36 (1):61 - 95.
Jeffrey Barrett (2007). Stability and Paradox in Algorithmic Logic. Journal of Philosophical Logic 36 (1):61 - 95.
J. W. Degen (1999). Complete Infinitary Type Logics. Studia Logica 63 (1):85-119.
Pawel Urzyczyn (1999). The Emptiness Problem for Intersection Types. Journal of Symbolic Logic 64 (3):1195-1215.
Added to index2009-01-28
Total downloads4 ( #460,364 of 1,779,220 )
Recent downloads (6 months)1 ( #291,352 of 1,779,220 )
How can I increase my downloads?