Abstract | ||
---|---|---|
We study the problem of type-checking functional programs in three extensions of ML. One distinguishing feature of these extensions is that they allow recursive definitions to be polymorphically typed. Although the motivation for these extensions comes from pragmatic considerations of programming language design, we show that the typability problem for each one of these extensions is polynomial-time equivalent to the Semi-Unification Problem and, therefore, undecidable. |
Year | DOI | Venue |
---|---|---|
1993 | 10.1145/169701.169687 | ACM Trans. Program. Lang. Syst. |
Keywords | Field | DocType |
fixpoint operator,polymorphic abstraction,polymorphic recursion,semiunification,type reconstruction,polymorphism | Programming language,Computer science,Theoretical computer science,Polymorphic recursion,Recursion,Undecidable problem,Mathematical logic | Journal |
Volume | Issue | ISSN |
15 | 2 | 0164-0925 |
Citations | PageRank | References |
46 | 3.28 | 16 |
Authors | ||
3 |
Name | Order | Citations | PageRank |
---|---|---|---|
A. J. Kfoury | 1 | 461 | 47.34 |
Jerzy Tiuryn | 2 | 229 | 22.79 |
P. Urzyczyn | 3 | 200 | 18.28 |