zbMATH — the first resource for mathematics

Globular: an online proof assistant for higher-dimensional rewriting. (English) Zbl 1387.68206
Kesner, Delia (ed.) et al., 1st international conference on formal structures for computation and deduction, FSCD 2016, Porto, Portugal, June 22–26, 2016. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-95977-010-1). LIPIcs – Leibniz International Proceedings in Informatics 52, Article 34, 11 p. (2016).
Summary: 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.
For the entire collection see [Zbl 1351.68020].

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68Q42 Grammars and rewriting systems
Agda; Coq; Globular; Orchard
Full Text: DOI