scientific article; zbMATH DE number 1301735

MaRDI QIDQ4246948zbMATH OpenFDO

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

Publication date 13 December 1999

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

• scientific article; zbMATH DE number 1086673
• 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:

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