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...
Expand abstract
- Publication status:
- Published
- Peer review status:
- Peer reviewed
Actions
Authors
Funding
Bibliographic Details
- Publisher:
- Schloss Dagstuhl Publisher's website
- 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:
Item Description
- 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)
Metrics
If you are the owner of this record, you can report an update to it here: Report update to this record