Typed operational semantics for higher-order subtyping.

DOI10.1016/S0890-5401(03)00062-2MaRDI QIDQ1401950zbMATH OpenFDO

Authors Adriana Compagnoni, Healfdene Goguen

Publication date 19 August 2003

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

Full work available at URL https://doi.org/10.1016/S0890-5401(03)00062-2

zbMATH Keywords

\(\lambda\)-calculusDependent kindsSubtypingType theoryTyped-operational semantics

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55)

Recommendations

• scientific article; zbMATH DE number 2079017
• Higher-order subtyping and its decidability
• Syntactic Metatheory of Higher-Order Subtyping
• Higher-order subtyping
• scientific article; zbMATH DE number 1231606

Cites work

• A characterization of F-complete type assignments
• A filter lambda model and the completeness of type assignment
• A modest model of records, inheritance, and bounded quantification
• A semantic basis for Quest
• A semantics of multiple inheritance
• A system of constructor classes: overloading and implicit higher-order polymorphism
• Coherence of subsumption, minimum typing and type-checking in F ≤
• Higher-order subtyping
• scientific article; zbMATH DE number 2185661 (Why is no real title available?)
• scientific article; zbMATH DE number 954811 (Why is no real title available?)
• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 51766 (Why is no real title available?)
• scientific article; zbMATH DE number 65534 (Why is no real title available?)
• scientific article; zbMATH DE number 108365 (Why is no real title available?)
• scientific article; zbMATH DE number 1301735 (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 720178 (Why is no real title available?)
• scientific article; zbMATH DE number 1142318 (Why is no real title available?)
• scientific article; zbMATH DE number 2079017 (Why is no real title available?)
• scientific article; zbMATH DE number 944097 (Why is no real title available?)
• scientific article; zbMATH DE number 814798 (Why is no real title available?)
• scientific article; zbMATH DE number 1424051 (Why is no real title available?)
• scientific article; zbMATH DE number 226803 (Why is no real title available?)
• Intensional interpretations of functionals of finite type I
• Operations on records
• Parallel reductions in \(\lambda\)-calculus
• Subtyping dependent types
• Typed operational semantics for higher-order subtyping.

Cited in

(12)

• Typed operational semantics for higher-order subtyping.
• Relational interpretations of recursive types in an operational setting.
• Dependent types with subtyping and late-bound overloading
• Strong normalization with singleton types
• Polarised subtyping for sized types
• Syntactic Metatheory of Higher-Order Subtyping
• scientific article; zbMATH DE number 1231606 (Why is no real title available?)
• Taming the merge operator
• Anti-symmetry of higher-order subtyping and equality by subtyping
• Subtyping dependent types
• Higher-order subtyping and its decidability
• Type-directed operational semantics for gradual typing

Describes a project that uses

Uses Software

• Automath
• PolyTOIL

This page was built for publication: Typed operational semantics for higher-order subtyping.

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1401950)