### Abstract

Induction-induction is a priciple for mutually defining data types A : Set and B : A Set. Both A and B are defined inductively, and the constructors for A can refer to B and vice versa.

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

Title of host publication | Logic, Construction, Computation |

Editors | Ulrich Berger, Diener Hannes, Peter Schuster, Monika Seisenberger |

Pages | 259 - 287 |

Volume | 3 |

DOIs | |

Publication status | Published - 2012 |

### Publication series

Name | Ontos mathematical logic |
---|---|

Publisher | Ontos Verlag |

### Keywords

- inductive-inductive definitions
- programming
- mathematical logic

## Cite this

Nordvall Forsberg, F., & Setzer, A. (2012). A finite axiomatisation of inductive-inductive definitions. In U. Berger, D. Hannes, P. Schuster, & M. Seisenberger (Eds.),

*Logic, Construction, Computation*(Vol. 3, pp. 259 - 287). (Ontos mathematical logic). https://doi.org/10.1515/9783110324921.259