- Ãø¼Ô
- Frank Pfenning
- ¥¿¥¤¥È¥ë
- On the Undecidability of Partial Polymorphic Type Reconstruction
- Æü»þ
- January 1992
- ³µÍ×
- We prove that partial type reconstruction for the pure
polymorphic ¦Ë-calculus is undecidable by a reduction
from the second-order unification problem, extending a previous
result by H.-J. Boehm.
We show further that partial type reconstruction remains
undecidable even in a very small predicative fragment of the
polymorphic ¦Ë-calculus, which implies undecidability
of partial type reconstruction for ¦ËML as introduced
by Harper, Mitchell, and Moggi.
¦Ë
^[$@&K^[(J^[$@&K^[(J^[$@&K^[(J^[$@&K^[(J^[$@&K^[(J^[$@&K^[(J
- ¥«¥Æ¥´¥ê
- CMUTR

Category: CMUTR
Institution: Department of Computer Science, Carnegie
Mellon University
Abstract: We prove that partial type reconstruction for the pure
polymorphic ¦Ë-calculus is undecidable by a reduction
from the second-order unification problem, extending a previous
result by H.-J. Boehm.
We show further that partial type reconstruction remains
undecidable even in a very small predicative fragment of the
polymorphic ¦Ë-calculus, which implies undecidability
of partial type reconstruction for ¦ËML as introduced
by Harper, Mitchell, and Moggi.
¦Ë
^[$@&K^[(J^[$@&K^[(J^[$@&K^[(J^[$@&K^[(J^[$@&K^[(J^[$@&K^[(J
Number: CMU-CS-92-105
Bibtype: TechReport
Month: jan
Author: Frank Pfenning
Title: On the Undecidability of Partial Polymorphic Type Reconstruction
Year: 1992
Address: Pittsburgh, PA
Super: @CMUTR