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.
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 available | 5 Apr 2023 |
|---|---|
| Publisher | Zenodo |
| Date of data production | 2019 |
Research output
- 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 AccessFile8 Link opens in a new tab Citations (Scopus)68 Downloads (Pure)
Projects
- 1 Finished
-
Homotopy Type Theory: Programming and Verification
Ghani, N. (Principal Investigator) & McBride, C. (Co-investigator)
EPSRC (Engineering and Physical Sciences Research Council)
1/04/15 → 30/09/19
Project: Research
Cite this
- DataSetCite