Projects per year
Abstract
We present three ordinal notation systems representing ordinals below epsilon zero in type theory, using recent type-theoretical innovations such as mutual inductive-inductive definitions and higher inductive types. We show how ordinal arithmetic can be developed for these systems, and how they admit a transfinite induction principle. We prove that all three notation systems are equivalent, so that we can transport results between them using the univalence principle. All our constructions have been implemented in cubical Agda.
Original language | English |
---|---|
Title of host publication | CPP 2020 : Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs |
Editors | Jasmin Blanchette, Catalin Hritcu |
Place of Publication | New York |
Pages | 172–185 |
Number of pages | 14 |
DOIs | |
Publication status | Published - 24 Jan 2020 |
Keywords
- theory of computation
- proof theory
- type theory
- ordinal notation
- cantor normal form
- inductive-inductive definitions
- higher inductive types
- cubical Agda
- programming
Profiles
-
Fredrik Nordvall Forsberg
- Computer And Information Sciences - Lecturer B
- SICSA
Person: Academic, Research Only
Projects
- 1 Finished
-
Homotopy Type Theory: Programming and Verification
EPSRC (Engineering and Physical Sciences Research Council)
1/04/15 → 30/09/19
Project: Research