Globular: an online proof assistant for higher-dimensional rewriting

Research output: Contribution to journalArticlepeer-review

Authors

Colleges, School and Institutes

External organisations

  • Radboud University, Nijmegen, The Netherlands
  • Department of Computer Science, University of Oxford

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.

Details

Original languageEnglish
Article number8
Number of pages16
JournalLogical Methods in Computer Science
Volume14
Issue number1
Publication statusPublished - 22 Jan 2018

Keywords

  • computer science , logic in computer science , mathematics , category theory