Title :
Type reconstruction in finite-rank fragments of the polymorphic λ-calculus
Author :
Kfoury, A.J. ; Tiuryn, J.
Author_Institution :
Dept. of Comput. Sci., Boston Univ., MA, USA
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
Keywords :
formal logic; inference mechanisms; DEXPTIME-complete; ML; finite-rank fragments; inference mechanisms; polymorphic λ-calculus; polynomial-time equivalent; type reconstruction; Calculus; Computer science; Computer science education; Polynomials;
Conference_Titel :
Logic in Computer Science, 1990. LICS '90, Proceedings., Fifth Annual IEEE Symposium on e
Conference_Location :
Philadelphia, PA
Print_ISBN :
0-8186-2073-0
DOI :
10.1109/LICS.1990.113728
