{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,28]],"date-time":"2022-03-28T22:24:44Z","timestamp":1648506284547},"reference-count":8,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":4394,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[2002,3]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The first system of intersection types. Coppo and Dezani [3], extended simple types to include intersections and added intersection introduction and elimination rules ((\u039b<jats:italic>I<\/jats:italic> ) and (\u039b<jats:italic>E<\/jats:italic>) ) to the type assignment system. The major advantage of these new types was that they were invariant under <jats:italic>\u03b2<\/jats:italic>-equality, later work by Barendregt, Coppo and Dezani [1], extended this to include an (\u03b7) rule which gave types invariant under <jats:italic>\u03b2<\/jats:italic>\u03b7-reduction.<\/jats:p><jats:p>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 [5] that this emptiness problem is decidable for the sytem including (\u03b7). but without (\u039b<jats:italic>I<\/jats:italic>).<\/jats:p><jats:p>The aim of this paper is to classify intersection type systems lacking some of (\u039b<jats:italic>I<\/jats:italic>), (\u039b<jats:italic>E<\/jats:italic>) and (\u03b7), into equivalence classes according to their strength in typing \u03bb-terms and also according to their strength in possessing inhabitants.<\/jats:p><jats:p>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.<\/jats:p>","DOI":"10.2178\/jsl\/1190150049","type":"journal-article","created":{"date-parts":[[2007,12,13]],"date-time":"2007-12-13T14:12:10Z","timestamp":1197555130000},"page":"353-368","source":"Crossref","is-referenced-by-count":0,"title":["A classification of intersection type systems"],"prefix":"10.1017","volume":"67","author":[{"given":"M. W.","family":"Bunder","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200010045_ref006","first-page":"1195","article-title":"The emptiness problem for intersection types","volume":"64","author":"Urzyczyn","year":"1999","journal-title":"Proceedings of logic in computer science"},{"key":"S0022481200010045_ref005","first-page":"297","volume-title":"TLCA '95","volume":"902","author":"Kurata","year":"1995"},{"key":"S0022481200010045_ref008","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/4.2.109"},{"key":"S0022481200010045_ref001","first-page":"931","volume":"48","author":"Barendregt","year":"1983","journal-title":"A filter lambda model and the completeness of type assignment"},{"key":"S0022481200010045_ref003","doi-asserted-by":"publisher","DOI":"10.1007\/BF02011875"},{"key":"S0022481200010045_ref004","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211394"},{"key":"S0022481200010045_ref007","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90297-S"},{"key":"S0022481200010045_ref002","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/10.4.357"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200010045","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,6]],"date-time":"2019-05-06T21:34:53Z","timestamp":1557178493000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200010045\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,3]]},"references-count":8,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2002,3]]}},"alternative-id":["S0022481200010045"],"URL":"https:\/\/doi.org\/10.2178\/jsl\/1190150049","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[2002,3]]}}}