The emptiness problem for intersection types

Journal of Symbolic Logic 64 (3):1195-1215 (1999)
  Copy   BIBTEX


We study the intersection type assignment system as defined by Barendregt, Coppo and Dezani. For the four essential variants of the system (with and without a universal type and with and without subtyping) we show that the emptiness (inhabitation) problem is recursively unsolvable. That is, there is no effective algorithm to decide if there is a closed term of a given type. It follows that provability in the logic of "strong conjunction" of Mints and Lopez-Escobar is also undecidable



    Upload a copy of this work     Papers currently archived: 74,509

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library


Added to PP

26 (#443,558)

6 months
1 (#417,896)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Typed Lambda Calculus.Henk P. Barendregt, Wil Dekkers & Richard Statman - 1977 - In Jon Barwise & H. Jerome Keisler (eds.), Handbook of Mathematical Logic. North-Holland Pub. Co.. pp. 1091--1132.
Typability and Type Checking in System F Are Equivalent and Undecidable.J. B. Wells - 1999 - Annals of Pure and Applied Logic 98 (1-3):111-156.

Add more citations

References found in this work

Functional Characters of Solvable Terms.M. Coppo, M. Dezani-Ciancaglini & B. Venneri - 1981 - Zeitschrift fur mathematische Logik und Grundlagen der Mathematik 27 (2-6):45-58.
Functional Characters of Solvable Terms.M. Coppo, M. Dezani-Ciancaglini & B. Venneri - 1981 - Mathematical Logic Quarterly 27 (2‐6):45-58.
The Formulae-as-Types Notion of Construction.William Alvin Howard - 1980 - In Haskell Curry, Hindley B., Seldin J. Roger & P. Jonathan (eds.), To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism. Academic Press.
The Completeness of Provable Realizability.G. E. Mints - 1989 - Notre Dame Journal of Formal Logic 30 (3):420-441.

View all 6 references / Add more references