Higher-order subtyping and its decidability
DOI10.1016/J.IC.2004.01.001zbMATH Open1055.03013OpenAlexW2016699565MaRDI QIDQ598199FDOQ598199
Authors: 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
Recommendations
DecidabilityBounded polymorphismHigher-order lambda calculusHigher-order subtypingIntersection types
Decidability of theories and sets of sentences (03B25) Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70) Functional programming and lambda calculus (68N18)
Cites Work
- A semantics of multiple inheritance
- An extension of basic functionality theory for \(\lambda\)-calculus
- Title not available (Why is that?)
- Title not available (Why is that?)
- On theories with a combinatorial definition of 'equivalence'
- A filter lambda model and the completeness of type assignment
- Title not available (Why is that?)
- Title not available (Why is that?)
- Some Properties of Conversion
- Operations on records
- Intensional interpretations of functionals of finite type I
- Title not available (Why is that?)
- Bounded existentials and minimal typing
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Inheritance as implicit coercion
- Order-sorted inductive types
- Combining type disciplines
- Higher-order subtyping
- Typed operational semantics for higher-order subtyping.
- A new type assignment for λ-terms
- Coherence of subsumption, minimum typing and type-checking in F ≤
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Simple type-theoretic foundations for object-oriented programming
- Title not available (Why is that?)
- Title not available (Why is that?)
- Subtyping dependent types
Cited In (10)
- On the decidability of subtyping with bounded existential types and implementation constraints
- The subtyping problem for second-order types is undecidable.
- Title not available (Why is that?)
- Analytic proof systems for \(\lambda\)-calculus: the elimination of transitivity, and why it matters
- Higher-order subtyping
- Typed operational semantics for higher-order subtyping.
- Syntactic Metatheory of Higher-Order Subtyping
- A decidable subtyping logic for intersection and union types
- Title not available (Why is that?)
- Anti-symmetry of higher-order subtyping and equality by subtyping
Uses Software
This page was built for publication: Higher-order subtyping and its decidability
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q598199)
