Cubical Agda formalization of Three equivalent ordinal notation systems

Dataset

Description

This is the complete cubical Agda formalisation of our CPP'20 paper "Three equivalent ordinal notation systems in cubical Agda".

Tested with:

- Agda development version 2.6.1 (commit: 4af7b92663d2eb1dd94383b140eb7acfeb1b1eb0)
- Cubical Agda library (commit: d7e345d3bcaefbc066d057487fca9677de7e29c7)

See index.lagda for a table of contents which includes all files. An html rendering of the cubical Agda code is available at Chuangjie Xu's GitHub web page (https://cj-xu.github.io/agda/ordinals/index.html).

GNU General Public License version 3

This site includes records provided by Elsevier's Data Monitor product. University of Strathclyde does not control or guarantee the accuracy, relevance, or completeness of the information contained in such records and accepts no responsibility or liability for such information.
Date made available5 Apr 2023
PublisherZenodo
Date of data production2019

Contact

  • 1 Conference contribution book

  • Three equivalent ordinal notation systems in cubical Agda

    Nordvall Forsberg, F., Xu, C. & Ghani, N., 24 Jan 2020, CPP 2020 : Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs. Blanchette, J. & Hritcu, C. (eds.). New York, p. 172–185 14 p.

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution book

    Open Access
    File
    7 Citations (Scopus)
    66 Downloads (Pure)

Cite this