Fibrational induction rules for initial algebras

DOI10.1007/978-3-642-15205-4_27MaRDI QIDQ3586050zbMATH OpenOpenAlexFDO

Authors Neil Ghani, Patricia Johann, Clément Fumex

Publication date 3 September 2010

Published in Computer Science Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-15205-4_27

Mathematics Subject Classification ID

Eilenberg-Moore and Kleisli constructions for monads (18C20) Functional programming and lambda calculus (68N18) Abstract data types; algebraic specification (68Q65)

Recommendations

• Generic fibrational induction
• Fibrational induction meets effects
• scientific article; zbMATH DE number 2079043
• Indexed induction and coinduction, fibrationally
• Indexed induction and coinduction, fibrationally

Cited in

(12)

• Structural induction and coinduction in a fibrational setting
• Deriving logical relations from interpretations of predicate logic
• Deep induction: induction rules for (truly) nested types
• From realizability to induction via dependent intersection
• Fibrational induction meets effects
• Generic fibrational induction
• scientific article; zbMATH DE number 2079043 (Why is no real title available?)
• Bisimulation as a logical relation
• The calculus of dependent lambda eliminations
• Indexed induction and coinduction, fibrationally
• Indexed induction and coinduction, fibrationally
• A fibrational tale of operational logical relations: pure, effectful and differential

This page was built for publication: Fibrational induction rules for initial algebras

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