Typed operational semantics for higher-order subtyping.

DOI10.1016/S0890-5401(03)00062-2zbMath1055.68075MaRDI QIDQ1401950

Adriana Compagnoni, Healfdene Goguen

Publication date: 19 August 2003

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

zbMATH Keywords

\(\lambda\)-calculusType theorySubtypingDependent kindsTyped-operational semantics

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55)

Related Items

Higher-order subtyping and its decidability, Typed operational semantics for higher-order subtyping., Polarised subtyping for sized types, Syntactic Metatheory of Higher-Order Subtyping, Subtyping dependent types, Strong Normalization with Singleton Types, Dependent types with subtyping and late-bound overloading, Taming the Merge Operator

Uses Software

• Automath
• PolyTOIL

Cites Work

• A modest model of records, inheritance, and bounded quantification
• A characterization of F-complete type assignments
• A semantics of multiple inheritance
• Higher-order subtyping
• Typed operational semantics for higher-order subtyping.
• A filter lambda model and the completeness of type assignment
• Operations on records
• Coherence of subsumption, minimum typing and type-checking in F ≤
• A system of constructor classes: overloading and implicit higher-order polymorphism
• A semantic basis for Quest
• Intensional interpretations of functionals of finite type I
• Parallel reductions in \(\lambda\)-calculus
• 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
• Unnamed Item
• Unnamed Item
• Unnamed Item