Electrical Engineering
      and Computer Sciences

Electrical Engineering and Computer Sciences

COLLEGE OF ENGINEERING

UC Berkeley

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