HackerPapers

arXiv:1612.01093cs.LO

Globular: an online proof assistant for higher-dimensional rewriting

Krzysztof Bar, Aleks Kissinger, Jamie Vicary

Early discovery. Linked by one identifiable commenter. This paper is outside the main ranking; a mention is not an endorsement.

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.

arXiv comments
Journal reference
Logical Methods in Computer Science, Volume 14, Issue 1 (January 22, 2018) lmcs:2579
DOI
doi:10.23638/LMCS-14(1:8)2018
Subjects
cs.LOLogic in Computer Science math.CTCategory Theory

On Hacker News

Linked by 1 identifiable commenter in 1 comment across 1 thread, from Mar 2018 to Mar 2018.

Comments linking this paper, per year.

Discussed in comments1 thread

  1. A self-contained, brief and complete formulation of Voevodsky's Univalence Axiom 1 comment

    • There are some developments, for example "Globular": https://arxiv.org/abs/1612.01093 I don't think there is a proof assistant that's really based on categorical foundations. I'd love to see something like that though.

      mbidView on HNParent context

Submitted to Hacker News

Connected through shared HN threads, not inferred similarity or a recommendation.