Machine-Checked Categorical Diagrammatic Reasoning
Fuente:
arXiv
Guardado en:
| Autores principales: | , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2024
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866916141975207936 |
|---|---|
| author | Guillemet, Benoît Mahboubi, Assia Piquerez, Matthieu |
| author_facet | Guillemet, Benoît Mahboubi, Assia Piquerez, Matthieu |
| contents | This paper describes a formal proof library, developed using the Coq proof assistant, designed to assist users in writing correct diagrammatic proofs, for 1-categories. This library proposes a deep-embedded, domain-specific formal language, which features dedicated proof commands to automate the synthesis, and the verification, of the technical parts often eluded in the literature. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2402_14485 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Machine-Checked Categorical Diagrammatic Reasoning Guillemet, Benoît Mahboubi, Assia Piquerez, Matthieu Logic in Computer Science F.4.1; G.4 This paper describes a formal proof library, developed using the Coq proof assistant, designed to assist users in writing correct diagrammatic proofs, for 1-categories. This library proposes a deep-embedded, domain-specific formal language, which features dedicated proof commands to automate the synthesis, and the verification, of the technical parts often eluded in the literature. |
| title | Machine-Checked Categorical Diagrammatic Reasoning |
| topic | Logic in Computer Science F.4.1; G.4 |
| url | https://arxiv.org/abs/2402.14485 |