|
Published Articles >> Table of Contents >> Abstract
21st Annual IEEE Symposium on Logic in Computer Science (LICS'06)
pp. 111-122
On Typability for Rank-2 Intersection Types with Polymorphic Recursion
Tachio Terauchi, University of California, Berkeley, USA
Alex Aiken, Stanford University, USA
Full Article Text:
 
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/LICS.2006.41
Send link to a friend
| 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.
|
 Additional Information
|
Citation:
Tachio Terauchi, Alex Aiken,
"On Typability for Rank-2 Intersection Types with Polymorphic Recursion,"
lics,
pp. 111-122,
21st Annual IEEE Symposium on Logic in Computer Science (LICS'06),
2006
|
|
