Inductive-inductive definitions

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

12 Citations (Scopus)

Abstract

We present a principle for introducing new types in type theory which generalises strictly positive indexed inductive data types. In this new principle a set A is defined inductively simultaneously with an A-indexed set B, which is also defined inductively. Compared to indexed inductive definitions, the novelty is that the index set A is generated inductively simultaneously with B. In other words, we mutually define two inductive sets, of which one depends on the other.
Instances of this principle have previously been used in order to formalise type theory inside type theory. However the consistency of the framework used (the theorem prover Agda) is not so clear, as it allows the definition of a universe containing a code for itself. We give an axiomatisation of the new principle in such a way that the resulting type theory is consistent, which we prove by constructing a set-theoretic model.
Original languageEnglish
Title of host publicationComputer Science Logic
Subtitle of host publication24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23-27, 2010. Proceedings
EditorsAnuj Dawar, Helmut Veith
Place of PublicationBerlin
Pages454-468
Number of pages15
DOIs
Publication statusPublished - 11 Aug 2010
Event24th International Workshop on Computer Science Logic, CSL 2010, and 19th Annual Conference of the EACSL - Brno, Czech Republic
Duration: 23 Aug 201027 Aug 2010

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
Volume6247
ISSN (Print)0302-9743

Conference

Conference24th International Workshop on Computer Science Logic, CSL 2010, and 19th Annual Conference of the EACSL
CountryCzech Republic
CityBrno
Period23/08/1027/08/10

Keywords

  • axiomatisation
  • data type
  • inductive definitions
  • theorem provers
  • theoretical model
  • type theory

Cite this