A Graphical Interface for Category Theory Proofs in Coq
Fuente:
arXiv
Gespeichert in:
| 1. Verfasser: | |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866912382892113920 |
|---|---|
| author | Chabassier, Luc |
| author_facet | Chabassier, Luc |
| contents | The importance of category theory in recent developments in both mathematics and in computer science cannot be overstated. However, its abstract nature makes it difficult to understand at first. Graphical languages have been developed to help manage this abstraction, but they have not been used in proof assistants, most of which are text-based. We believe that a graphical interface for categorical proofs integrated in a generic proof assistant would allow students to familiarize themselves with diagrammatic reasoning on concrete proofs that they are already familiar with. We present an implementation of a Coq plugin that enables both visualization and interactions with Coq proofs in a graphical manner. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2505_13473 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | A Graphical Interface for Category Theory Proofs in Coq Chabassier, Luc Logic in Computer Science Programming Languages D.2.4; F.4.1 The importance of category theory in recent developments in both mathematics and in computer science cannot be overstated. However, its abstract nature makes it difficult to understand at first. Graphical languages have been developed to help manage this abstraction, but they have not been used in proof assistants, most of which are text-based. We believe that a graphical interface for categorical proofs integrated in a generic proof assistant would allow students to familiarize themselves with diagrammatic reasoning on concrete proofs that they are already familiar with. We present an implementation of a Coq plugin that enables both visualization and interactions with Coq proofs in a graphical manner. |
| title | A Graphical Interface for Category Theory Proofs in Coq |
| topic | Logic in Computer Science Programming Languages D.2.4; F.4.1 |
| url | https://arxiv.org/abs/2505.13473 |