A finite axiomatisation of inductive-inductive definitions

Fredrik Nordvall Forsberg, Anton Setzer

Research output: Chapter in Book/Report/Conference proceeding › Other 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

Access to Document

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