Structural subtyping for inductive types with functorial equality rules

DOI10.1017/S0960129508006956zbMATH Open1156.68017OpenAlexW2157934017MaRDI QIDQ3535679FDOQ3535679

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

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

zbMATH Keywords

coercive subtyping

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• A framework for defining logics
• Title not available (Why is that?)
• Title not available (Why is that?)
• Inheritance as implicit coercion
• Subtyping dependent types
• The view from the left
• Coercive subtyping
• Coercion completion and conservativity in coercive subtyping
• Transitivity in coercive subtyping
• An implementation of LF with coercive subtyping and universes

Cited In (2)

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

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)