Transitivity in coercive subtyping

DOI10.1016/J.IC.2004.10.008zbMATH Open1064.03021OpenAlexW2000702491MaRDI QIDQ1776403FDOQ1776403

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

Recommendations

• Coherence and Transitivity in Coercive Subtyping
• scientific article; zbMATH DE number 2003159
• scientific article; zbMATH DE number 1086673
• Coherence and transitivity of subtyping as entailment
• Coercion completion and conservativity in coercive subtyping
• Coercive subtyping via mappings of reduction behaviour
• scientific article; zbMATH DE number 1301735
• Implicit coercions in type systems
• Coercive subtyping: theory and implementation
• Coercive subtyping for the calculus of constructions (extended abstract)

zbMATH Keywords

transitivitysubtyping in dependent type theories with inductive types

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• A framework for defining logics
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Coercive subtyping
• Title not available (Why is that?)
• Type inference with simple subtypes
• Title not available (Why is that?)
• Coherence and transitivity of subtyping as entailment
• Coherence and Transitivity in Coercive Subtyping
• Coercion completion and conservativity in coercive subtyping
• Title not available (Why is that?)
• Title not available (Why is that?)
• An implementation of LF with coercive subtyping and universes

Cited In (7)

• Title not available (Why is that?)
• Manifest Fields and Module Mechanisms in Intensional Type Theory
• Structural subtyping for inductive types with functorial equality rules
• Types for Proofs and Programs
• Coercive subtyping via mappings of reduction behaviour
• Coherence and Transitivity in Coercive Subtyping
• Coercions in a polymorphic type system

Uses Software

• Coq
• Plastic
• 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)