文章基本信息

标题：Globular: An Online Proof Assistant for Higher-Dimensional Rewriting
本地全文：下载
作者：Krzysztof Bar ; Aleks Kissinger ; Jamie Vicary 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2016
卷号：52
页码：34:1-34:11
DOI：10.4230/LIPIcs.FSCD.2016.34
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：higher category theory; higher-dimensional rewriting; interactive theorem proving