Thursday 25 May 2023, 14:00, room 1Z76: An interface for diagrammatic proofs in Coq, Luc Chabassier (LMF).

Commutative diagrams are an intuitive and powerful way to reason about equational systems in category theory. However, their graphical nature means they can't really be encoded in text based proof assistants, such as Coq. To tackle this, we developed a Coq plugin that can extract such a graph from the context of the proof, and display it in an interface, allowing reasoning directly on the graph. Furthermore, once the interaction is finished a Coq proof term is generated that corresponds to the manipulations done to the graph.