Machine-Checked Categorical Diagrammatic Reasoning
Logic in Computer Science
2024-03-01 v4
Abstract
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.
Cite
@article{arxiv.2402.14485,
title = {Machine-Checked Categorical Diagrammatic Reasoning},
author = {Benoît Guillemet and Assia Mahboubi and Matthieu Piquerez},
journal= {arXiv preprint arXiv:2402.14485},
year = {2024}
}