On typability for rank-2 intersection types with polymorphic recursion

Tachio Terauchi, Alex Aiken

Research output: Chapter in Book/Report/Conference proceedingConference contribution

3 Citations (Scopus)

Abstract

We show that typability for a natural form of polymorphic recursive typing for rank-2 intersection types is undecidable. Our proof involves characterizing typability as a context free language (CFL) graph problem, which may be of independent interest, and reduction from the boundedness problem for Turing machines. We also show a property of the type system which, in conjunction with the undecidability result, disproves a misconception about the Milner-Mycroft type system. We also show undecidability of a related program analysis problem.

Original languageEnglish
Title of host publicationProceedings - 21st Annual IEEE Symposium on Logic in Computer Science, LICS 2006
Pages111-120
Number of pages10
DOIs
Publication statusPublished - 2006 Dec 1
Event21st Annual IEEE Symposium on Logic in Computer Science, LICS 2006 - Seattle, WA, United States
Duration: 2006 Aug 122006 Aug 15

Publication series

NameProceedings - Symposium on Logic in Computer Science
ISSN (Print)1043-6871

Other

Other21st Annual IEEE Symposium on Logic in Computer Science, LICS 2006
CountryUnited States
CitySeattle, WA
Period06/8/1206/8/15

ASJC Scopus subject areas

  • Software
  • Mathematics(all)

Fingerprint Dive into the research topics of 'On typability for rank-2 intersection types with polymorphic recursion'. Together they form a unique fingerprint.

  • Cite this

    Terauchi, T., & Aiken, A. (2006). On typability for rank-2 intersection types with polymorphic recursion. In Proceedings - 21st Annual IEEE Symposium on Logic in Computer Science, LICS 2006 (pp. 111-120). [1691222] (Proceedings - Symposium on Logic in Computer Science). https://doi.org/10.1109/LICS.2006.41