Search

• < Previous
• 1
• Next >

---

Generic Fibrational Induction

Neil Ghani ; Patricia Johann ; Clement Fumex.

This paper provides an induction rule that can be used to prove properties of data structures whose types are inductive, i.e., are carriers of initial algebras of functors. Our results are semantic in nature and are inspired by Hermida and Jacobs' elegant algebraic formulation of induction for&nbsp;[&hellip;]

---

Indexed Induction and Coinduction, Fibrationally

Neil Ghani ; Patricia Johann ; Clement Fumex.

This paper extends the fibrational approach to induction and coinduction pioneered by Hermida and Jacobs, and developed by the current authors, in two key directions. First, we present a dual to the sound induction rule for inductive types that we developed previously. That is, we present a sound&nbsp;[&hellip;]

---