Transitivity in coercive subtyping

DOI10.1016/J.IC.2004.10.008MaRDI QIDQ1776403zbMATH OpenOpenAlexFDO

Authors Zhaohui Luo, Yong Luo

Publication date 12 May 2005

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

Full work available at URL https://doi.org/10.1016/j.ic.2004.10.008

zbMATH Keywords

subtyping in dependent type theories with inductive typestransitivity

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Logic in computer science (03B70) Second- and higher-order arithmetic and fragments (03F35)

Recommendations

• Coherence and Transitivity in Coercive Subtyping
• Weak transitivity in coercive subtyping
• Coercive subtyping in type theory
• Coherence and transitivity of subtyping as entailment
• Coercion completion and conservativity in coercive subtyping
• Coercive subtyping via mappings of reduction behaviour
• Some algorithmic and proof-theoretical aspects of coercive subtyping
• Implicit coercions in type systems
• Coercive subtyping: theory and implementation
• Coercive subtyping for the calculus of constructions (extended abstract)

Cites work

• A framework for defining logics
• An implementation of LF with coercive subtyping and universes
• Coercion completion and conservativity in coercive subtyping
• Coercive subtyping
• Coercive subtyping in type theory
• Coherence and Transitivity in Coercive Subtyping
• Coherence and transitivity of subtyping as entailment
• Constructor subtyping in the calculus of inductive constructions
• scientific article; zbMATH DE number 4180771 (Why is no real title available?)
• scientific article; zbMATH DE number 3910392 (Why is no real title available?)
• scientific article; zbMATH DE number 50149 (Why is no real title available?)
• scientific article; zbMATH DE number 65535 (Why is no real title available?)
• scientific article; zbMATH DE number 512790 (Why is no real title available?)
• scientific article; zbMATH DE number 591911 (Why is no real title available?)
• scientific article; zbMATH DE number 1497808 (Why is no real title available?)
• Type inference with simple subtypes
• Weak transitivity in coercive subtyping

Cited in

(7)

• Coercive subtyping via mappings of reduction behaviour
• Coherence and Transitivity in Coercive Subtyping
• Coercions in a polymorphic type system
• Structural subtyping for inductive types with functorial equality rules
• Manifest Fields and Module Mechanisms in Intensional Type Theory
• Weak transitivity in coercive subtyping
• Combining incoherent coercions for -types

Describes a project that uses

Uses Software

• Plastic
• Coq
• LEGO

This page was built for publication: Transitivity in coercive subtyping

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