Globular: an online proof assistant for higher-dimensional rewritingArticle
Authors: Krzysztof Bar ; Aleks Kissinger ; Jamie Vicary
NULL##NULL##NULL
Krzysztof Bar;Aleks Kissinger;Jamie Vicary
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.
Deep Drug Discovery and Deployment; Code: PTDC/CCI-BIO/29266/2017
Quantum Computation, Logic, and Security; Funder: European Commission; Code: 320571
Bibliographic References
3 Documents citing this article
John D. Foley;Spencer Breiner;Eswaran Subrahmanian;John M. Dusel, 2021, Operads for complex system design specification, analysis and synthesis, Proceedings - Royal Society. Mathematical, physical and engineering sciences (Print), 477, 2250, 10.1098/rspa.2021.0099, https://doi.org/10.1098/rspa.2021.0099.