The subtyping problem for second-order types is undecidable.

DOI10.1006/inco.2001.2950zbMath1049.68039OpenAlexW3180721729WikidataQ61634972 ScholiaQ61634972MaRDI QIDQ1400717

Paweł Urzyczyn, Jerzy Tiuryn

Publication date: 2002

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://semanticscholar.org/paper/5b88628bf9711f01e38366241044d9ccb951944a

zbMATH Keywords

type-checkingpolymorphic lambda-calculus

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Functional programming and lambda calculus (68N18)

Related Items (4)

A language for generic programming in the large ⋮ Subtyping recursion and parametric polymorphism in kernel Fun ⋮ Intersection, Universally Quantified, and Reference Types ⋮ Typability and type checking in System F are equivalent and undecidable

Cites Work

• Unnamed Item
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Polymorphic type inference and containment
• Typability and type checking in System F are equivalent and undecidable
• Bounded quantification is undecidable
• Equational axiomatization of bicoercibility for polymorphic types

This page was built for publication: The subtyping problem for second-order types is undecidable.