Tachio Terauchi and Alex Aiken
EECS Department
University of California, Berkeley
Technical Report No. UCB/EECS-2006-66
May 18, 2006
http://www2.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://www2.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://www2.eecs.berkeley.edu/Pubs/TechRpts/2006/EECS-2006-66.html %F Terauchi:EECS-2006-66