2024/02/22 by Guillemet, Benoît, Mahboubi, Assia, Piquerez, Matthieu
#F.4.1 #FOS: Computer and information sciences #G.4 #Logic in Computer Science (cs.LO)
paper · doi:10.48550/arxiv.2402.14485
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.