TY - GEN
T1 - On typability for rank-2 intersection types with polymorphic recursion
AU - Terauchi, Tachio
AU - Aiken, Alex
N1 - Copyright:
Copyright 2011 Elsevier B.V., All rights reserved.
PY - 2006
Y1 - 2006
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=34547346635&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=34547346635&partnerID=8YFLogxK
U2 - 10.1109/LICS.2006.41
DO - 10.1109/LICS.2006.41
M3 - Conference contribution
AN - SCOPUS:34547346635
SN - 0769526314
SN - 9780769526317
T3 - Proceedings - Symposium on Logic in Computer Science
SP - 111
EP - 120
BT - Proceedings - 21st Annual IEEE Symposium on Logic in Computer Science, LICS 2006
T2 - 21st Annual IEEE Symposium on Logic in Computer Science, LICS 2006
Y2 - 12 August 2006 through 15 August 2006
ER -