Some algorithmic and proof-theoretical aspects of coercive subtyping

DOI10.1007/BFB0097792MaRDI QIDQ4246948zbMATH OpenFDO

Authors Alex K. Jones, Zhaohui Luo, Serguei V. Solov'ev

Publication date 13 December 1999

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/BFB0097792

zbMATH Keywords

coercive subtypingproof-theoretic and computational propertiessubset relationshipstype theory

Mathematics Subject Classification ID

Logic in computer science (03B70) Second- and higher-order arithmetic and fragments (03F35)

Recommendations

• Coercive subtyping in type theory
• Coercive subtyping
• Coherence and Transitivity in Coercive Subtyping
• Coercive subtyping: theory and implementation

Cited in

(13)

• Typed operational semantics for higher-order subtyping.
• Transitivity in coercive subtyping
• scientific article; zbMATH DE number 1617290 (Why is no real title available?)
• Coherence and Transitivity in Coercive Subtyping
• Subset Coercions in Coq
• Refinement Types as Proof Irrelevance
• scientific article; zbMATH DE number 1156716 (Why is no real title available?)
• Relating Church-style and Curry-style subtyping
• A framework for type inference with subtyping
• Theoretical Computer Science
• An implementation of LF with coercive subtyping and universes
• Coercion completion and conservativity in coercive subtyping
• Integrating coercion with subtyping and multiple dispatch

Describes a project that uses

Uses Software

• LEGO

This page was built for publication: Some algorithmic and proof-theoretical aspects of coercive subtyping

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