The Subtyping Problem for Second-Order Types Is Undecidable

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.

Authors

• Jerzy Tiuryn
• Paweł Urzyczyn

Keywords

No keywords are indexed for this paper.