On Typability for Rank-2 Intersection Types with Polymorphic Recursion

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 MilnerMycroft type system. We also show undecidability of a related program analysis problem.

• Type: Conference
• Year: 2006
• Where: LICS
• Authors: Tachio Terauchi, Alex Aiken
• Keywords: Computer Science, LICS 2006, Polymorphic Recursive Typing, Rank-2 Intersection Types, Type System