Paper: The Subtyping Problem for Second-Order Types is Undecidable (at LICS 1996)
Authors: Jerzy Tiuryn Pawel UrzyczynAbstract
We prove that the subtyping problem induced by Mitchell's containment relation 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.
BibTeX
@InProceedings{TiurynUrzyczyn-TheSubtypingProblem, author = {Jerzy Tiuryn and Pawel Urzyczyn}, title = {The Subtyping Problem for Second-Order Types is Undecidable}, booktitle = {Proceedings of the Eleventh Annual IEEE Symp. on Logic in Computer Science, {LICS} 1996}, year = 1996, editor = {Edmund M. Clarke}, month = {July}, pages = {74-85}, location = {New Brunswick, NJ, USA}, publisher = {IEEE Computer Society Press} }