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