Paper: Type reconstruction in finite-rank fragments of the polymorphic λ-calculus (at LICS 1990)
Authors: Assaf J. Kfoury Jerzy Tiuryn
Abstract
It is proven that the problem of type reconstruction in the polymorphic λ-calculus of rank two is polynomial-time equivalent to the problem of type reconstruction in ML, and is therefore DEXPTIME-complete. It is also proven that for every k>2, the problem of type reconstruction in the polymorphic λ-calculus of rank k, extended with suitably chosen constants with types of rank one, is undecidable
BibTeX
@InProceedings{KfouryTiuryn-Typereconstructioni, author = {Assaf J. Kfoury and Jerzy Tiuryn}, title = {Type reconstruction in finite-rank fragments of the polymorphic λ-calculus }, booktitle = {Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science (LICS 1990)}, year = {1990}, month = {June}, pages = {2--11}, location = {Philadelphia, PA, USA}, publisher = {IEEE Computer Society Press} }