Three equivalent ordinal notation systems in cubical Agda

Nordvall Forsberg, Fredrik and Xu, Chuangjie and Ghani, Neil; Blanchette, Jasmin and Hritcu, Catalin, eds. (2020) Three equivalent ordinal notation systems in cubical Agda. In: CPP 2020 : Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs. ACM, New York, 172–185. ISBN 9781450370974

[thumbnail of Forsberg-etal-SIGPLAN-2020-Three-equivalent-ordinal-notation-systems-in-cubical-agda]
Preview
 Text (Forsberg-etal-SIGPLAN-2020-Three-equivalent-ordinal-notation-systems-in-cubical-agda)
Forsberg_etal_SIGPLAN_2020_Three_equivalent_ordinal_notation_systems_in_cubical_agda.pdf
Accepted Author Manuscript
Download (860kB)| Preview

    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.

    ORCID iDs

    Nordvall Forsberg, Fredrik ORCID logoORCID: https://orcid.org/0000-0001-6157-9288, Xu, Chuangjie and Ghani, Neil ORCID logoORCID: https://orcid.org/0000-0002-3988-2560; Blanchette, Jasmin and Hritcu, Catalin
    • Item type:Book Section
      ID code:71215
      Dates:
      Date
      Event
      24 January 2020
      Published
      27 November 2019
      Accepted
      Keywords:theory of computation, proof theory, type theory, ordinal notation, cantor normal form, inductive-inductive definitions, higher inductive types, cubical Agda, programming, Electronic computers. Computer science, Computational Theory and Mathematics
      Subjects:Science > Mathematics > Electronic computers. Computer science
      Department:Faculty of Science > Computer and Information Sciences
      Depositing user: Pure Administrator
      Date deposited:27 Jan 2020 13:32
      Last modified:31 Mar 2021 00:58
      URI:https://strathprints.strath.ac.uk/id/eprint/71215
    CORE (COnnecting REpositories)