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},
    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