Globular: an online proof assistant for higher-dimensional rewriting
Published version
Peer-reviewed
Repository URI
Repository DOI
Change log
Authors
Vicary, Jamie
Bar, K
Kissinger, A
Abstract
This article introduces Globular, an online proof assistant for the formalization and veri cation 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.
Description
Keywords
Journal Title
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).
Conference Name
Journal ISSN
0000-0000
Volume Title
14
Publisher
Episciences.org