### Abstract

This paper provides several induction rules that can be used to prove properties of effectful data types. Our results are semantic in nature and build upon Hermida and Jacobs’ fibrational formulation of induction for polynomial data types and its extension to all inductive data types by Ghani, Johann, and Fumex. An effectful data type μ(TF) is built from a functor F that describes data, and a monad T that computes effects. Our main contribution is to derive induction rules that are generic over all functors F and monads T such that μ(TF) exists. Along the way, we also derive a principle of definition by structural recursion for effectful data types that is similarly generic. Our induction rule is also generic over the kinds of properties to be proved: like the work on which we build, we work in a general fibrational setting and so can accommodate very general notions of properties, rather than just those of particular syntactic forms. We give examples exploiting the generality of our results, and show how our results specialize to those in the literature, particularly those of Filinski and Støvring.

Original language | English |
---|---|

Title of host publication | Foundations of Software Science and Computational Structures |

Subtitle of host publication | 15th International Conference, FOSSACS 2011 |

Editors | Lars Birkedal |

Publisher | Springer |

Pages | 42-57 |

Number of pages | 16 |

Volume | 7213 |

DOIs | |

Publication status | Published - 2012 |

Event | 15th International Conference, FOSSACS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012 - Tallinn, Estonia Duration: 24 Mar 2012 → 1 Apr 2012 |

### Publication series

Name | Lecture Notes in Computer Science |
---|---|

Publisher | Springer |

Volume | 7213 |

ISSN (Print) | 0302-9743 |

### Conference

Conference | 15th International Conference, FOSSACS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012 |
---|---|

Abbreviated title | FOSSACS 2012 |

Country | Estonia |

City | Tallinn |

Period | 24/03/12 → 1/04/12 |

### Keywords

- fibrational induction
- polynomial data types

## Fingerprint Dive into the research topics of 'Fibrational induction meets effects'. Together they form a unique fingerprint.

## Cite this

Atkey, R., Ghani, N., Jacobs, B., & Johann, P. (2012). Fibrational induction meets effects. In L. Birkedal (Ed.),

*Foundations of Software Science and Computational Structures: 15th International Conference, FOSSACS 2011*(Vol. 7213, pp. 42-57). (Lecture Notes in Computer Science; Vol. 7213). Springer. https://doi.org/10.1007/978-3-642-28729-9_3