Skip to main content
SpringerLink
Log in

Inhabitation of Low-Rank Intersection Types

  • Conference paper
Book cover Typed Lambda Calculi and Applications (TLCA 2009)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 5608))

Included in the following conference series:

Abstract

We prove that the inhabitation problem (“Does there exist a closed term of a given type?”) is undecidable for intersection types of rank 3 and exponential space complete for intersection types of rank 2.

Partly supported by Ministry of Science and Higher Education grant N N206 355836.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Alessi, F., Barbanera, F.: Strong conjunction and intersection types. In: Tarlecki, A. (ed.) MFCS 1991. LNCS, vol. 520, pp. 64–73. Springer, Heidelberg (1991)

    Chapter  Google Scholar 

  2. Alessi, F., Barbanera, F., Dezani-Ciancaglini, M.: Intersection types and lambda models. Theoretical Computer Science 355(2), 108–126 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  3. Bunder, M.W.: The inhabitation problem for intersection types. In: Harland, J., Manyem, P. (eds.) Computing: The Australasian Theory Symposium. Conferences in Research and Practice in Information Technology, vol. 77, pp. 7–14. Australian Computer Society (2008)

    Google Scholar 

  4. Coppo, M., Dezani-Ciancaglini, M.: An extension of basic functionality theory for lambda-calculus. Notre Dame Journal of Formal Logic 21, 685–693 (1980)

    Article  MathSciNet  MATH  Google Scholar 

  5. Dezani-Ciancaglini, M., Ghilezan, S., Venneri, B.: The “relevance” of intersection and union types. Notre Dame Journal of Formal Logic 38(2), 246–269 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  6. Kfoury, A.J., Wells, J.B.: Principality and type inference for intersection types using expansion variables. Theoretical Computer Science 311(1–3), 1–70 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  7. Kozen, D.: Automata and Computability. Undergraduate Texts in Computer Science. Springer, Heidelberg (1997)

    Book  MATH  Google Scholar 

  8. Kozen, D.: Theory of Computation. Springer, Heidelberg (2006)

    MATH  Google Scholar 

  9. Kurata, T., Takahashi, M.: Decidable properties of intersection type systems. In: Dezani-Ciancaglini, M., Plotkin, G. (eds.) TLCA 1995. LNCS, vol. 902, pp. 297–311. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  10. Kuśmierek, D.: The inhabitation problem for rank two intersection types. In: Ronchi Della Rocca, S. (ed.) TLCA 2007. LNCS, vol. 4583, pp. 240–254. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  11. Leivant, D.: Polymorphic type inference. In: PoPL, pp. 88–98. ACM Press, New York (1983)

    Google Scholar 

  12. Liquori, L., Ronchi Della Rocca, S.: Intersection-types à la Church. Information and Computation 205(9), 1371–1386 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  13. Lopez-Escobar, E.G.K.: Proof functional connectives. In: Methods in Mathematical Logic. LNMath, vol. 1130, pp. 208–221. Springer, Heidelberg (1993)

    Chapter  Google Scholar 

  14. Mints, G.E.: The completeness of provable realizability. Notre Dame Journal of Formal Logic 30, 420–441 (1989)

    Article  MathSciNet  MATH  Google Scholar 

  15. Møller Neergaard, P., Mairson, H.G.: Types, potency, and idempotency: Why nonlinearity and amnesia make a type system work. In: ICFP, pp. 138–149. ACM Press, New York (2004)

    Google Scholar 

  16. Pottinger, G.: A type assingment for the strongly normalizable λ-terms. In: Seldin, J.P., Hindley, J.R. (eds.) To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 561–577. Academic Press, London (1980)

    Google Scholar 

  17. Ronchi Della Rocca, S., Roversi, L.: Intersection logic. In: Fribourg, L. (ed.) CSL 2001. LNCS, vol. 2142, pp. 414–428. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  18. Sørensen, M.H., Urzyczyn, P.: Lectures on the Curry-Howard Isomorphism. Elsevier, Amsterdam (2006)

    MATH  Google Scholar 

  19. TLCA List of Open Problems, http://tlca.di.unito.it/opltlca/

  20. Urzyczyn, P.: The emptiness problem for intersection types. Journal of Symbolic Logic 64(3), 1195–1215 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  21. Venneri, B.: Intersection types as logical formulae. Journal of Logic and Computation 4(2), 109–124 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  22. Wells, J.B., Haack, C.: Branching types. In: Le Métayer, D. (ed.) ESOP 2002. LNCS, vol. 2305, pp. 115–132. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  23. Yokouchi, H.: Embedding a second-order type system into an intersection type system. Information and Computation 117(2), 206–220 (1995)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Informatics, University of Warsaw, Poland

    Paweł Urzyczyn

Authors
  1. Paweł Urzyczyn
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Laboratoire PPS (CNRS / Paris 7), Case 7014, Université Paris Diderot - Paris 7, 75205, Paris Cedex 13, France

    Pierre-Louis Curien

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Urzyczyn, P. (2009). Inhabitation of Low-Rank Intersection Types. In: Curien, PL. (eds) Typed Lambda Calculi and Applications. TLCA 2009. Lecture Notes in Computer Science, vol 5608. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02273-9_26

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-02273-9_26

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-02272-2

  • Online ISBN: 978-3-642-02273-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation