Syntactic Metatheory of Higher-Order Subtyping

DOI10.1007/978-3-540-87531-4_32MaRDI QIDQ3540196zbMATH OpenOpenAlexFDO

Authors Andreas Abel, Dulma Rodriguez

Publication date 20 November 2008

Published in Computer Science Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-87531-4_32

zbMATH Keywords

algorithmic subtypingbounded quantificationhereditary substitutionhigher-order subtyping

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Higher-order subtyping and its decidability
• scientific article; zbMATH DE number 2079017
• Higher-order subtyping
• Polarized Subtyping for Sized Types
• Polarised subtyping for sized types

Cites work

• An algebraic interpretation of the K-calculus; and an application of a labelled -calculus
• Anti-symmetry of higher-order subtyping and equality by subtyping
• Higher-order subtyping
• scientific article; zbMATH DE number 42059 (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?)
• Implementing a normalizer using sized heterogeneous types
• Mechanizing metatheory in a logical framework
• Polarized Subtyping for Sized Types
• Towards a mechanized metatheory of Standard ML
• Typed operational semantics for higher-order subtyping.
• Types and programing languages
• Types for Proofs and Programs
• Types for Proofs and Programs

Cited in

(8)

• Typed operational semantics for higher-order subtyping.
• Syntactically restricting bounded polymorphism for decidable subtyping
• Polarized Subtyping for Sized Types
• Polarised subtyping for sized types
• scientific article; zbMATH DE number 2079017 (Why is no real title available?)
• Hereditary substitution for the \(\lambda \Delta \)-calculus
• Higher-order subtyping and its decidability
• Fast verified BCD subtyping

This page was built for publication: Syntactic Metatheory of Higher-Order Subtyping

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