A finite axiomatisation of inductive-inductive definitions

Research output: Chapter in Book/Report/Conference proceedingOther chapter contribution


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 languageEnglish
Title of host publicationLogic, Construction, Computation
EditorsUlrich Berger, Diener Hannes, Peter Schuster, Monika Seisenberger
Pages259 - 287
Publication statusPublished - 2012

Publication series

NameOntos mathematical logic
PublisherOntos Verlag


  • inductive-inductive definitions
  • programming
  • mathematical logic


Dive into the research topics of 'A finite axiomatisation of inductive-inductive definitions'. Together they form a unique fingerprint.

Cite this