Higher-order subtyping

DOI10.1016/S0304-3975(96)00096-5zbMath0903.68020MaRDI QIDQ1392282

Martin Steffen, Benjamin C. Pierce

Publication date: 23 July 1998

Published in: Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

polymorphismtype systemslambda-calculussubtypingbounded quantificationtypechecking

Mathematics Subject Classification ID

Theory of programming languages (68N15)

Related Items (12)

Higher-order subtyping and its decidability ⋮ Typed operational semantics for higher-order subtyping. ⋮ Polarised subtyping for sized types ⋮ Syntactic Metatheory of Higher-Order Subtyping ⋮ Type-Based Termination with Sized Products ⋮ A Tutorial on Type-Based Termination ⋮ Coherence of subsumption for monadic types ⋮ Full Abstraction in a Subtyped pi-Calculus with Linear Types ⋮ Order-sorted inductive types ⋮ Basic theory of \(F\)-bounded quantification. ⋮ Comparing object encodings. ⋮ Taming the Merge Operator

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Divergence of \(F_{\leq}\) type checking
• A modest model of records, inheritance, and bounded quantification
• A semantics of multiple inheritance
• Bounded existentials and minimal typing
• The lambda calculus, its syntax and semantics
• Inheritance as implicit coercion
• An extension of system \(F\) with subtyping
• Bounded quantification is undecidable
• A new type assignment for λ-terms
• Coherence of subsumption, minimum typing and type-checking in F ≤
• Subtyping + extensionality: Confluence of βηtop reduction in F≤

This page was built for publication: Higher-order subtyping