Transitivity in coercive subtyping

DOI10.1016/j.ic.2004.10.008zbMath1064.03021OpenAlexW2000702491MaRDI QIDQ1776403

Yong Luo, Zhaohui 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

transitivitysubtyping in dependent type theories with inductive types

Mathematics Subject Classification ID

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

Related Items (3)

Coercions in a polymorphic type system ⋮ Structural subtyping for inductive types with functorial equality rules ⋮ Manifest Fields and Module Mechanisms in Intensional Type Theory

Uses Software

• Coq
• Plastic
• LEGO

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Coherence and Transitivity in Coercive Subtyping
• A framework for defining logics
• Coercive subtyping
• Coherence and transitivity of subtyping as entailment
• Type inference with simple subtypes
• An implementation of LF with coercive subtyping and universes
• Coercion completion and conservativity in coercive subtyping

This page was built for publication: Transitivity in coercive subtyping