University of Birmingham > Talks@bham > Theoretical computer science seminar > A Fibrational Induction Rule for Inductive Types

A Fibrational Induction Rule for Inductive Types

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Paul Levy.

We develop a generic induction rule that can be used to prove properties of inductive data types. Our results are semantic in nature and are inspired by Hermida and Jacobs’ elegant algebraic formulation of induction for polynomial data types. Our contribution is to derive, under slightly different assumptions, an induction rule that is generic over all inductive types, polynomial or not. Our induction rule is generic over the kinds of properties to be proved as well over the data types to which the properties refer. Like Hermida and Jacobs, we work in a general fibrational setting and so can accommodate very general notions of properties on inductive types rather than just those of particular syntactic forms. The correctness of our generic induction rule is proved by reducing induction to iteration. We show how our rule can be instantiated to give induction rules for non-polynomial data types such as rose trees, finite hereditary sets, and hyperfunctions. Our instantiation for hyperfunctions underscores the value of working in the general fibrational setting since this data type cannot be interpreted as a set.

This is joint work with Neil Ghani and Clement Fumex.

This talk is part of the Theoretical computer science seminar series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on from the University of Cambridge.