Conference item
Globular: an online proof assistant for higher-dimensional rewriting
- Abstract:
-
This article introduces Globular, an online proof assistant for the formalization and verification of proofs in higher-dimensional category theory. The tool produces graphical visualizations of higher-dimensional proofs, assists in their construction with a point-and-click interface, and performs type checking to prevent incorrect rewrites. Hosted on the web, it has a low barrier to use, and allows hyperlinking of formalized proofs directly from research papers. It allows the formalization of proofs from logic, topology and algebra which are not formalizable by other methods, and we give several examples. Interest in the tool has been strong, with 4126 sessions across 884 unique users in the first 2 months since deployment.
- Publication status:
- Published
- Peer review status:
- Peer reviewed
Actions
Access Document
- Files:
-
-
(Preview, Version of record, pdf, 1.1MB, Terms of use)
-
- Publisher copy:
- 10.4230/LIPIcs.FSCD.2016.34
Authors
- Publisher:
- Schloss Dagstuhl
- Host title:
- Leibniz International Proceedings in Informatics
- Volume:
- Formal Structures for Computation and Deduction (FSCD) 2016
- Publication date:
- 2016-06-01
- Acceptance date:
- 2016-04-06
- DOI:
- Keywords:
- Subjects:
- Pubs id:
-
pubs:614784
- UUID:
-
uuid:8787f0d0-f811-477a-87f3-8c3ac1ab0ba2
- Local pid:
-
pubs:614784
- Source identifiers:
-
614784
- Deposit date:
-
2016-04-10
Terms of use
- Copyright holder:
- Bar et al
- Copyright date:
- 2016
- Notes:
-
© Krzysztof Bar, Aleks Kissinger, and Jamie Vicary;
licensed under Creative Commons License CC-BY
1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). http://fscd2016.dcc.fc.up.pt/
- Licence:
- CC Attribution (CC BY)
If you are the owner of this record, you can report an update to it here: Report update to this record