Higher-order subtyping and its decidability

DOI10.1016/j.ic.2004.01.001zbMath1055.03013OpenAlexW2016699565MaRDI QIDQ598199

Adriana Compagnoni

Publication date: 6 August 2004

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

Full work available at URL: https://doi.org/10.1016/j.ic.2004.01.001

zbMATH Keywords

DecidabilityBounded polymorphismHigher-order lambda calculusHigher-order subtypingIntersection types

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Decidability of theories and sets of sentences (03B25) Combinatory logic and lambda calculus (03B40)

Related Items (1)

Analytic proof systems for \(\lambda\)-calculus: the elimination of transitivity, and why it matters

Uses Software

• Automath
• Forsythe

Cites Work

• A semantics of multiple inheritance
• Bounded existentials and minimal typing
• An extension of basic functionality theory for \(\lambda\)-calculus
• Inheritance as implicit coercion
• Order-sorted inductive types
• Combining type disciplines
• Higher-order subtyping
• Typed operational semantics for higher-order subtyping.
• On theories with a combinatorial definition of 'equivalence'
• A new type assignment for λ-terms
• A filter lambda model and the completeness of type assignment
• Operations on records
• Coherence of subsumption, minimum typing and type-checking in F ≤
• Simple type-theoretic foundations for object-oriented programming
• Intensional interpretations of functionals of finite type I
• Some Properties of Conversion
• Subtyping dependent types
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Higher-order subtyping and its decidability