Title :
The subtyping problem for second-order types is undecidable
Author :
Tiuryn, Jerzy ; Urzyczyn, Pawel
Author_Institution :
Inst. of Inf., Warsaw Univ., Poland
Abstract :
We prove that the subtyping problem induced by Mitchell´s containment relation (1988) for second-order polymorphic types is undecidable. It follows that type-checking is undecidable for the polymorphic lambda-calculus extended by an appropriate subsumption rule
Keywords :
decidability; lambda calculus; programming theory; type theory; containment relation; polymorphic lambda-calculus; second-order polymorphic types; second-order types; subsumption rule; subtyping problem; type-checking; Iron; Terminology;
Conference_Titel :
Logic in Computer Science, 1996. LICS '96. Proceedings., Eleventh Annual IEEE Symposium on
Conference_Location :
New Brunswick, NJ
Print_ISBN :
0-8186-7463-6
DOI :
10.1109/LICS.1996.561306
