Structural subtyping for inductive types with functorial equality rules

DOI10.1017/S0960129508006956zbMath1156.68017OpenAlexW2157934017MaRDI QIDQ3535679

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)

Related Items (1)

Manifest Fields and Module Mechanisms in Intensional Type Theory

Uses Software

• Plastic
• LEGO

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Inheritance as implicit coercion
• Transitivity in coercive subtyping
• A framework for defining logics
• Coercive subtyping
• The view from the left
• An implementation of LF with coercive subtyping and universes
• Coercion completion and conservativity in coercive subtyping
• Subtyping dependent types

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