Higher Homotopies in a Hierarchy of Univalent Universes
- Submitting institution
-
University of Nottingham, The
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 4784611
- Type
- D - Journal article
- DOI
-
10.1145/2729979
- Title of journal
- ACM Transactions on Computational Logic
- Article number
- 18
- First page
- -
- Volume
- 16
- Issue
- 2
- ISSN
- 1529-3785
- Open access status
- Out of scope for open access requirements
- Month of publication
- April
- Year of publication
- 2015
- URL
-
-
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
1
- Research group(s)
-
-
- Citation count
- 4
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- Univalent Foundations offer a new approach to proof assistants and dependently typed programming. This paper solves one of the open problems of the Princeton IAS special year (2012/13) on the topic. The submitting author received the Ackermann Award, the international distinguished dissertation prize by the European Association for Computer Science Logic, as the sole winner in 2016. The jury cites the contribution of this paper as a main reason for their decision. The jury's report is the first chapter of the proceedings of CSL'16, available at: https://drops.dagstuhl.de/opus/portals/lipics/index.php?semnr=16017
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -
