Output details
11 - Computer Science and Informatics
Swansea University
Output title
A Categorical Semantics for Inductive-Inductive Definitions
Type
E - Conference contribution
Name of conference/published proceedings
Algebra and Coalgebra in Computer Science. 4th International Conference, CALCO 2011, Winchester, UK, August 30 – September 2, 2011. Proceedings
Volume number
6859
Issue number
-
First page of article
70
ISSN of proceedings
0302-9743
Year of publication
2011
URL
-
Number of additional authors
3
Additional information
<11> Inductive-inductive definitions are supported by the theorem prover Agda but were lacking a proper theoretical foundation. They have been used for proving theorems about Martin-Löf Type Theory (MLTT) inside MLTT. They are used in the new area of Homotopy Type Theory (http://homotopytypetheory.org) based at the Institute of Advanced Studies, Princeton, where they formalise real numbers and Conway's surreal numbers. In this article a generalisation of initial algebras to dialgebras is used to provide a better foundation and formalisation of induction-induction.
Interdisciplinary
-
Cross-referral requested
-
Research group
A - Theoretical Computer Science
Citation count
0
Proposed double-weighted
No
Double-weighted statement
-
Reserve for a double-weighted output
No
Non-English
No
English abstract
-
