Rencontre,
27 juin 2024
Matthieu Piquerez (Galinette, INRIA), Machine-Checked Categorical Diagrammatic Reasoning
Schedule
- 27 juin 2024, 13:45 - 14:45
Abstract
We describe 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.
Joint work with Benoît Guillemet and Assia Mahboubi, see https://arxiv.org/abs/2402.14485