Krzysztof Bar ; Aleks Kissinger ; Jamie Vicary - Globular: an online proof assistant for higher-dimensional rewriting

lmcs:2579 - Logical Methods in Computer Science, January 22, 2018, Volume 14, Issue 1 - https://doi.org/10.23638/LMCS-14(1:8)2018
Globular: an online proof assistant for higher-dimensional rewritingArticle

Authors: 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.


    Volume: Volume 14, Issue 1
    Published on: January 22, 2018
    Accepted on: July 19, 2017
    Submitted on: July 19, 2017
    Keywords: Computer Science - Logic in Computer Science,Mathematics - Category Theory
    Funding:
      Source : OpenAIRE Graph
    • Deep Drug Discovery and Deployment; Code: PTDC/CCI-BIO/29266/2017
    • Quantum Computation, Logic, and Security; Funder: European Commission; Code: 320571

    3 Documents citing this article

    Consultation statistics

    This page has been seen 1857 times.
    This article's PDF has been downloaded 407 times.