Globular: an online proof assistant for higher-dimensional rewriting
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 t...
| Main Authors: | , , |
|---|---|
| Format: | Journal article |
| Published: |
Logical Methods in Computer Science e.V.
2018
|
| _version_ | 1797097650388992000 |
|---|---|
| author | Bar, K Kissinger, A Vicary, J |
| author_facet | Bar, K Kissinger, A Vicary, J |
| author_sort | Bar, K |
| collection | OXFORD |
| description | 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. |
| first_indexed | 2024-03-07T04:58:30Z |
| format | Journal article |
| id | oxford-uuid:d7719f28-7108-41e1-8524-1a42ca1b1f8a |
| institution | University of Oxford |
| last_indexed | 2024-03-07T04:58:30Z |
| publishDate | 2018 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | dspace |
| spelling | oxford-uuid:d7719f28-7108-41e1-8524-1a42ca1b1f8a2022-03-27T08:41:08ZGlobular: an online proof assistant for higher-dimensional rewritingJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:d7719f28-7108-41e1-8524-1a42ca1b1f8aSymplectic Elements at OxfordLogical Methods in Computer Science e.V.2018Bar, KKissinger, AVicary, JThis 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. |
| spellingShingle | Bar, K Kissinger, A Vicary, J Globular: an online proof assistant for higher-dimensional rewriting |
| title | Globular: an online proof assistant for higher-dimensional rewriting |
| title_full | Globular: an online proof assistant for higher-dimensional rewriting |
| title_fullStr | Globular: an online proof assistant for higher-dimensional rewriting |
| title_full_unstemmed | Globular: an online proof assistant for higher-dimensional rewriting |
| title_short | Globular: an online proof assistant for higher-dimensional rewriting |
| title_sort | globular an online proof assistant for higher dimensional rewriting |
| work_keys_str_mv | AT bark globularanonlineproofassistantforhigherdimensionalrewriting AT kissingera globularanonlineproofassistantforhigherdimensionalrewriting AT vicaryj globularanonlineproofassistantforhigherdimensionalrewriting |