A finite axiomatisation of inductive-inductive definitions

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

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

Publication series

NameOntos mathematical logic
PublisherOntos Verlag

Keywords

  • inductive-inductive definitions
  • programming
  • mathematical logic

Cite this