Picture map of Europe with pins indicating European capital cities

Open Access research with a European policy impact...

The Strathprints institutional repository is a digital archive of University of Strathclyde's Open Access research outputs. Strathprints provides access to thousands of Open Access research papers by Strathclyde researchers, including by researchers from the European Policies Research Centre (EPRC).

EPRC is a leading institute in Europe for comparative research on public policy, with a particular focus on regional development policies. Spanning 30 European countries, EPRC research programmes have a strong emphasis on applied research and knowledge exchange, including the provision of policy advice to EU institutions and national and sub-national government authorities throughout Europe.

Explore research outputs by the European Policies Research Centre...

Strathprints

A categorical semantics for inductive-inductive definitions

Altenkirch, Thorsten and Morris, Peter and Nordvall Forsberg, Fredrik and Setzer, Anton (2011) A categorical semantics for inductive-inductive definitions. In: Algebra and Coalgebra in Computer Science. Lecture Notes in Computer Science . Springer Berlin/Heidelberg, Berlin, pp. 70-84. ISBN 9783642229435

Full text not available in this repository. Request a copy from the Strathclyde author

Abstract

Induction-induction is a principle for defining data types in Martin-Löf Type Theory. An inductive-inductive definition consists of a set A, together with an A-indexed family B : A → Set, where both A and B are inductively defined in such a way that the constructors for A can refer to B and vice versa. In addition, the constructors for B can refer to the constructors for A. We extend the usual initial algebra semantics for ordinary inductive data types to the inductive-inductive setting by considering dialgebras instead of ordinary algebras. This gives a new and compact formalisation of inductive-inductive definitions, which we prove is equivalent to the usual formulation with elimination rules.

Item type: Book Section
ID code: 53101
Keywords: data type, dialgebras, elimination rules, formalisation, initial algebras, type theory, Electronic computers. Computer science, Computer Science(all)
Subjects: Science > Mathematics > Electronic computers. Computer science
Department: Faculty of Science > Computer and Information Sciences
Depositing user: Pure Administrator
Date deposited: 27 May 2015 13:38
Last modified: 09 Jun 2017 03:45
Related URLs:
URI: https://strathprints.strath.ac.uk/id/eprint/53101
Export data:
CORE (COnnecting REpositories)