Globular: an online proof assistant for higher-dimensional rewriting

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

Authors

Colleges, School and Institutes

External organisations

  • University of Oxford
  • Radboud University, Nijmegen, The Netherlands

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
Title of host publicationProceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
EditorsDelia Kesner, Brigitte Pientka
Publication statusPublished - 16 Jun 2016
Event1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016) - Porto, Portugal
Duration: 22 Jun 201626 Jun 2016

Publication series

NameLeibniz International Proceedings in Informatics (LIPIcs)
PublisherSchloss Dagstuhl-Leibniz-Zentrum fuer Informatik
Volume52
ISSN (Electronic)1868-8969

Conference

Conference1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
CountryPortugal
CityPorto
Period22/06/1626/06/16

Keywords

  • higher category theory, higher-dimensional rewriting, interactive theorem proving