The beta version of DROPS 2 is now publicly available! Check this page out at DROPS 2 now!


License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2016.34
URN: urn:nbn:de:0030-drops-59880
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2016/5988/
Go to the corresponding LIPIcs Volume Portal

Bar, Krzysztof ; Kissinger, Aleks ; Vicary, Jamie

Globular: An Online Proof Assistant for Higher-Dimensional Rewriting

pdf-format:
LIPIcs-FSCD-2016-34.pdf (1 MB)

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.

BibTeX - Entry

@InProceedings{bar_et_al:LIPIcs:2016:5988,
  author =	{Krzysztof Bar and Aleks Kissinger and Jamie Vicary},
  title =	{{Globular: An Online Proof Assistant for Higher-Dimensional Rewriting}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{34:1--34:11},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Delia Kesner and Brigitte Pientka},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2016/5988},
  URN =		{urn:nbn:de:0030-drops-59880},
  doi =		{10.4230/LIPIcs.FSCD.2016.34},
  annote =	{Keywords: higher category theory, higher-dimensional rewriting, interactive theorem proving}
}

Keywords: higher category theory, higher-dimensional rewriting, interactive theorem proving
Collection: 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
Issue Date: 2016
Date of publication: 17.06.2016

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI