@inbook{02b2e99a8e03483c8886e70700230d7b,
title = "A finite axiomatisation of inductive-inductive definitions",
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.",
keywords = "inductive-inductive definitions, programming, mathematical logic",
author = "{Nordvall Forsberg}, Fredrik and Anton Setzer",
year = "2012",
doi = "10.1515/9783110324921.259",
language = "English",
isbn = "9783110324921",
volume = "3",
series = "Ontos mathematical logic",
publisher = "Ontos Verlag",
pages = "259 -- 287",
editor = "Ulrich Berger and Diener Hannes and Peter Schuster and Monika Seisenberger",
booktitle = "Logic, Construction, Computation",
}