Constructions with Non-Recursive Higher Inductive Types
- Submitting institution
-
University of Nottingham, The
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 1330110
- Type
- E - Conference contribution
- DOI
-
10.1145/2933575.2933586
- Title of conference / published proceedings
- LICS '16: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science
- First page
- 595
- Volume
- 2016-July
- Issue
- -
- ISSN
- -
- Open access status
- -
- Month of publication
- July
- Year of publication
- 2016
- 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
-
0
- Research group(s)
-
-
- Citation count
- 3
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- Homotopy type theory offers a new approach to dependently typed programming and proof assistants. The central new concept of the field (so-called higher inductive types) was only partially understood when the paper was written, and the paper shows that a very simple special case of the concept is already sufficient to perform a core construction. For example, this is beneficial when using the Lean proof assistant (Microsoft Research), which only supports precisely this special case. The paper was published at the leading conference in the field (LICS, CORE A*-rated) and the result is fully formalised and computer-checked.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -
