## Paper: Type reconstruction in finite-rank fragments of the polymorphic λ-calculus (at LICS 1990)

Authors:**Kfoury, A.J. Tiuryn, J.**

### 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 = {Kfoury, A.J. and Tiuryn, J.}, title = {Type reconstruction in finite-rank fragments of the polymorphic λ-calculus }, booktitle = {Proceedings of the Fifth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1990}, year = 1990, editor = {John Mitchell}, month = {June}, pages = {2--11}, location = {Philadelphia, PA, USA}, publisher = {IEEE Computer Society Press} }