Globular: an online proof assistant for higher-dimensional rewriting
- Submitting institution
-
University of Cambridge
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 1945
- Type
- D - Journal article
- DOI
-
10.23638/LMCS-14(1:8)2018
- Title of journal
- Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Kesner, D. & Pientka, B. (eds.). Schloss Dagstuhl, p. 34:1-34:11 11 p. (Leibniz International Proceedings in Informatics (LIPIcs); vol. 52).
- Article number
- -
- First page
- 8
- Volume
- 14
- Issue
- 1
- ISSN
- 0000-0000
- Open access status
- Compliant
- Month of publication
- January
- Year of publication
- 2018
- 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
-
2
- Research group(s)
-
-
- Citation count
- 5
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- This work gave the first description of our proof assistant for higher algebra, called 'Globular', which has gone on to be highly influential in the category theory community, having been loaded 23,604 times by 5,964 users since launch in December 2015. The corresponding theory paper was published in the conference LICS. This proof assistant was first-in-class, allowing for the first time direct point-and-click manipulation of sophisticated geometrical composites in high dimension. It was the starting point for what has become a major research programme, including a large EPSRC grant.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -