Indexed induction and coinduction, fibrationally

DOI10.2168/LMCS-9(3:6)2013MaRDI QIDQ5891134zbMATH OpenOpenAlexFDO

Authors Neil Ghani, Patricia Johann, Clément Fumex

Publication date 6 September 2013

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.2168/lmcs-9(3:6)2013

zbMATH Keywords

coinductionfibrationsinduction

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65)

Recommendations

• Indexed induction and coinduction, fibrationally
• Structural induction and coinduction in a fibrational setting
• Generic fibrational induction
• Fibrational induction rules for initial algebras
• Fibred data types

Cited in

(13)

• Structural induction and coinduction in a fibrational setting
• Predicate and relation liftings for coalgebras with side effects: an application in coalgebraic modal logic
• Dependent types and fibred computational effects
• Induction, coinduction, and adjoints
• Fibrational induction meets effects
• Generic fibrational induction
• Fibrational induction rules for initial algebras
• Coinductive predicates and final sequences in a fibration
• An Isbell duality theorem for type refinement systems
• Dependent inductive and coinductive types are fibrational dialgebras
• Inductive and Coinductive Topological Generation with Church's thesis and the Axiom of Choice
• Fibred data types
• Indexed induction and coinduction, fibrationally

This page was built for publication: Indexed induction and coinduction, fibrationally

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