Higher-order subtyping and its decidability

DOI10.1016/J.IC.2004.01.001MaRDI QIDQ598199zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

DecidabilityBounded polymorphismHigher-order lambda calculusHigher-order subtypingIntersection types

Mathematics Subject Classification ID

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)

Recommendations

• scientific article; zbMATH DE number 2079017
• Higher-order subtyping
• Syntactic Metatheory of Higher-Order Subtyping
• scientific article; zbMATH DE number 814799
• Typed operational semantics for higher-order subtyping.

Cites work

• scientific article; zbMATH DE number 3875232 (Why is no real title available?)
• scientific article; zbMATH DE number 954811 (Why is no real title available?)
• scientific article; zbMATH DE number 47007 (Why is no real title available?)
• scientific article; zbMATH DE number 108365 (Why is no real title available?)
• scientific article; zbMATH DE number 512787 (Why is no real title available?)
• scientific article; zbMATH DE number 615137 (Why is no real title available?)
• scientific article; zbMATH DE number 2079017 (Why is no real title available?)
• scientific article; zbMATH DE number 1512607 (Why is no real title available?)
• scientific article; zbMATH DE number 944097 (Why is no real title available?)
• scientific article; zbMATH DE number 814792 (Why is no real title available?)
• scientific article; zbMATH DE number 814801 (Why is no real title available?)
• scientific article; zbMATH DE number 1391399 (Why is no real title available?)
• scientific article; zbMATH DE number 3400430 (Why is no real title available?)
• A filter lambda model and the completeness of type assignment
• A new type assignment for λ-terms
• A semantics of multiple inheritance
• An extension of basic functionality theory for \(\lambda\)-calculus
• Bounded existentials and minimal typing
• Coherence of subsumption, minimum typing and type-checking in F ≤
• Combining type disciplines
• Higher-order subtyping
• Inheritance as implicit coercion
• Intensional interpretations of functionals of finite type I
• On theories with a combinatorial definition of 'equivalence'
• Operations on records
• Order-sorted inductive types
• Simple type-theoretic foundations for object-oriented programming
• Some Properties of Conversion
• Subtyping dependent types
• Typed operational semantics for higher-order subtyping.

Cited in

(10)

• Syntactic Metatheory of Higher-Order Subtyping
• scientific article; zbMATH DE number 2079017 (Why is no real title available?)
• Analytic proof systems for \(\lambda\)-calculus: the elimination of transitivity, and why it matters
• A decidable subtyping logic for intersection and union types
• Higher-order subtyping
• Typed operational semantics for higher-order subtyping.
• On the decidability of subtyping with bounded existential types and implementation constraints
• The subtyping problem for second-order types is undecidable.
• scientific article; zbMATH DE number 1424051 (Why is no real title available?)
• Anti-symmetry of higher-order subtyping and equality by subtyping

Describes a project that uses

Uses Software

• Automath
• Forsythe

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)