@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",

}