# On Typability for Rank-2 Intersection Types with Polymorphic Recursion

### Tachio Terauchi and Alex Aiken

###
EECS Department

University of California, Berkeley

Technical Report No. UCB/EECS-2006-66

May 18, 2006

### http://www.eecs.berkeley.edu/Pubs/TechRpts/2006/EECS-2006-66.pdf

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 citation:

@techreport{Terauchi:EECS-2006-66, Author = {Terauchi, Tachio and Aiken, Alex}, Title = {On Typability for Rank-2 Intersection Types with Polymorphic Recursion}, Institution = {EECS Department, University of California, Berkeley}, Year = {2006}, Month = {May}, URL = {http://www.eecs.berkeley.edu/Pubs/TechRpts/2006/EECS-2006-66.html}, Number = {UCB/EECS-2006-66}, 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.} }

EndNote citation:

%0 Report %A Terauchi, Tachio %A Aiken, Alex %T On Typability for Rank-2 Intersection Types with Polymorphic Recursion %I EECS Department, University of California, Berkeley %D 2006 %8 May 18 %@ UCB/EECS-2006-66 %U http://www.eecs.berkeley.edu/Pubs/TechRpts/2006/EECS-2006-66.html %F Terauchi:EECS-2006-66