Coercion completion and conservativity in coercive subtyping

DOI10.1016/S0168-0072(01)00063-XzbMath1011.03017MaRDI QIDQ5957918

Serguei V. Solov'ev, Zhaohui Luo

Publication date: 29 May 2003

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

zbMATH Keywords

coercive subtypingdependent typestype-theory

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 (5)

Coercions in a polymorphic type system ⋮ Structural subtyping for inductive types with functorial equality rules ⋮ Transitivity in coercive subtyping ⋮ Manifest Fields and Module Mechanisms in Intensional Type Theory ⋮ Automorphisms of types in certain type theories and representation of finite groups

Uses Software

• Coq
• Plastic
• LEGO

Cites Work

• An extension of system \(F\) with subtyping
• Equational axiomatization of bicoercibility for polymorphic types
• Coercive subtyping
• Coherence and transitivity of subtyping as entailment
• An implementation of LF with coercive subtyping and universes
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Coercion completion and conservativity in coercive subtyping