Thesis

Investigations into inductive-recursive definitions

Creator
Rights statement
Awarding institution
  • University of Strathclyde
Date of award
  • 2015
Thesis identifier
  • T14039
Person Identifier (Local)
  • 201062463
Qualification Level
Qualification Name
Department, School or Faculty
Abstract
  • The theory of recursive functions where the domain of a function is inductively defined at the same time as the function is called induction-recursion. This theory has been introduced in Martin-Löf type theory by Dybjer and further explored in a series of papers by Dybjer and Setzer. Important data types like universes closed under dependent type operators are instances of this theory. In this thesis we study the class of data types arising from inductive-recursive definitions, taking the seminal work of Dybjer and Setzer as our starting point. We show how the theories of inductive and indexed inductive types arise as sub-theories of induction-recursion, by revealing the role played by a notion of of size within the theory of induction-recursion. We then expand the expressive power of induction-recursion, showing how to extend the theory of induction-recursion in two different ways: in one direction we investigate the changes needed to obtain a more flexible semantics which gives rise to a more comprehensive elimination principle for inductive-recursive types. In another direction we generalize the theory of induction-recursion to a fibrational setting. In both extensions we provide a finite axiomatization of the theories introduced, we show applications and examples of these theories not previously covered by induction-recursion, and we justify the existence of data types built within these theories.
Resource Type
DOI
Date Created
  • 2015
Former identifier
  • 1231571

Relations

Items