Globular: an online proof assistant for higher-dimensional rewriting

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Standard

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 proceedingConference contribution

Harvard

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

APA

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

Vancouver

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)). https://doi.org/10.4230/LIPIcs.FSCD.2016.34

Author

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

Bibtex

@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",

}

RIS

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

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 -