Paper: On Typability for Rank-2 Intersection Types with Polymorphic Recursion (at LICS 2006)

Authors: Tachio Terauchi Alexander Aiken

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.

BibTeX

  @InProceedings{TerauchiAiken-OnTypabilityforRank,
    author = 	 {Tachio Terauchi and Alexander Aiken},
    title = 	 {On Typability for Rank-2 Intersection Types with Polymorphic Recursion},
    booktitle =  {Proceedings of the Twenty-First Annual IEEE Symposium on Logic in Computer Science (LICS 2006)},
    year =	 {2006},
    month =	 {August}, 
    pages =      {111--120},
    location =   {Seattle, Washington, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }