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

This publication is archived. It is kept only for reference purposes, so it is no longer being updated and may not meet accessibility standards. If you need this content in a different format, please email webteam@eecs.berkeley.edu.

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2006/Archive/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