Structural subtyping for inductive types with functorial equality rules

DOI10.1017/S0960129508006956MaRDI QIDQ3535679zbMATH OpenOpenAlexFDO

Authors Zhaohui Luo, Robin Adams

Publication date 13 November 2008

Published in Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1017/s0960129508006956

zbMATH Keywords

coercive subtyping

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• scientific article; zbMATH DE number 2185708
• scientific article; zbMATH DE number 1183236
• Subtyping for F-bounded quantifiers and equirecursive types
• Equational theories for inductive types
• Logical equivalence for subtyping object and recursive types
• On the internal structures of inductive types
• Type inference with non-structural subtyping
• Subtyping and intersection types revisited
• scientific article; zbMATH DE number 1114034

Cites work

• scientific article; zbMATH DE number 50149 (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?)
• A framework for defining logics
• An implementation of LF with coercive subtyping and universes
• Coercion completion and conservativity in coercive subtyping
• Coercive subtyping
• Inheritance as implicit coercion
• Subtyping dependent types
• The view from the left
• Transitivity in coercive subtyping

Cited in

(2)

• Manifest Fields and Module Mechanisms in Intensional Type Theory
• Typed homomorphic relations extended with subtypes

Describes a project that uses

Uses Software

• Plastic
• LEGO

This page was built for publication: Structural subtyping for inductive types with functorial equality rules

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