Globular: an online proof assistant for higher-dimensional rewriting

Krzysztof  Bar; Aleks Kissinger; Jamie Vicary

doi:10.4230/LIPIcs.FSCD.2016.34

Globular: an online proof assistant for higher-dimensional rewriting

Krzysztof Bar, Aleks Kissinger, Jamie Vicary

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

7 Citations (Scopus)

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.

Original language	English
Title of host publication	Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
Editors	Delia Kesner, Brigitte Pientka
Publisher	Schloss Dagstuhl
Pages	34:1-34:11
Number of pages	11
ISBN (Print)	9783959770101
DOIs	https://doi.org/10.4230/LIPIcs.FSCD.2016.34
Publication status	Published - 16 Jun 2016
Event	1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016) - Porto, Portugal Duration: 22 Jun 2016 → 26 Jun 2016

Publication series

Name	Leibniz International Proceedings in Informatics (LIPIcs)
Publisher	Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik
Volume	52
ISSN (Electronic)	1868-8969

Conference

Conference	1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
Country/Territory	Portugal
City	Porto
Period	22/06/16 → 26/06/16

Keywords

higher category theory
higher-dimensional rewriting
interactive theorem proving

Access to Document

10.4230/LIPIcs.FSCD.2016.34Licence: Creative Commons: Attribution (CC BY)

Cite this

Bar, K., Kissinger, A., & Vicary, J. (2016). Globular: an online proof assistant for higher-dimensional rewriting. In D. Kesner, & B. Pientka (Eds.), Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016) (pp. 34:1-34:11). (Leibniz International Proceedings in Informatics (LIPIcs); Vol. 52). Schloss Dagstuhl. https://doi.org/10.4230/LIPIcs.FSCD.2016.34

Bar, Krzysztof ; Kissinger, Aleks ; Vicary, Jamie. / Globular: an online proof assistant for higher-dimensional rewriting. Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). editor / Delia Kesner ; Brigitte Pientka. Schloss Dagstuhl, 2016. pp. 34:1-34:11 (Leibniz International Proceedings in Informatics (LIPIcs)).

@inproceedings{b1ecaae16e324c2f96ae435435d9275c,

title = "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. ",

keywords = "higher category theory, higher-dimensional rewriting, interactive theorem proving",

author = "Krzysztof Bar and Aleks Kissinger and Jamie Vicary",

year = "2016",

month = jun,

day = "16",

doi = "10.4230/LIPIcs.FSCD.2016.34",

language = "English",

isbn = "9783959770101",

series = "Leibniz International Proceedings in Informatics (LIPIcs)",

publisher = "Schloss Dagstuhl",

pages = "34:1--34:11",

editor = "Delia Kesner and Pientka, \{Brigitte \}",

booktitle = "Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)",

address = "Germany",

note = "1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016) ; Conference date: 22-06-2016 Through 26-06-2016",

}

Bar, K, Kissinger, A & Vicary, J 2016, Globular: an online proof assistant for higher-dimensional rewriting. in D Kesner & B Pientka (eds), Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), vol. 52, Schloss Dagstuhl, pp. 34:1-34:11, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016), Porto, Portugal, 22/06/16. https://doi.org/10.4230/LIPIcs.FSCD.2016.34

Globular: an online proof assistant for higher-dimensional rewriting. / Bar, Krzysztof ; Kissinger, Aleks; Vicary, Jamie.
Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). ed. / Delia Kesner; Brigitte Pientka. Schloss Dagstuhl, 2016. p. 34:1-34:11 (Leibniz International Proceedings in Informatics (LIPIcs); Vol. 52).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Globular: an online proof assistant for higher-dimensional rewriting

AU - Bar, Krzysztof

AU - Kissinger, Aleks

AU - Vicary, Jamie

PY - 2016/6/16

Y1 - 2016/6/16

N2 - 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.

AB - 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.

KW - higher category theory

KW - higher-dimensional rewriting

KW - interactive theorem proving

UR - https://www.scopus.com/pages/publications/84977481240

U2 - 10.4230/LIPIcs.FSCD.2016.34

DO - 10.4230/LIPIcs.FSCD.2016.34

M3 - Conference contribution

SN - 9783959770101

T3 - Leibniz International Proceedings in Informatics (LIPIcs)

SP - 34:1-34:11

BT - Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)

A2 - Kesner, Delia

A2 - Pientka, Brigitte

PB - Schloss Dagstuhl

T2 - 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)

Y2 - 22 June 2016 through 26 June 2016

ER -

Bar K, Kissinger A, Vicary J. Globular: an online proof assistant for higher-dimensional rewriting. In Kesner D, Pientka B, editors, Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Schloss Dagstuhl. 2016. p. 34:1-34:11. (Leibniz International Proceedings in Informatics (LIPIcs)). doi: 10.4230/LIPIcs.FSCD.2016.34

Globular: an online proof assistant for higher-dimensional rewriting

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this