2026-08-21T18:02:50Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:27386 2026-08-21T14:42:37Z ddc:004 open_access

Diagrammatic Reasoning, Formally (Invited Talk) Pous, Damien Formal proofs graphical proofs string diagrams monoidal categories Kleene algebra relation algebra Rocq Modern proof assistants make it possible to verify theorems, but often makes it harder than with pen and paper. This is especially true in domains where proofs are best depicted using diagrams. For instance, confluence diagrams in rewriting theory, commuting diagrams in category theory, or string diagrams in monoidal categories. By using various tools and techniques to solve well-defined classes of goals, infer appropriate data, or perform high-level reasoning steps [Dexter Kozen, 1997; André Joyal and Ross Street, 1991], I will show how to obtain robust and elegant proof scripts in these application domains [Damien Pous, 2013; Damien Pous, 2026]. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Damien Pous 2026 Is Part Of LIPIcs, Volume 386, 51st International Symposium on Mathematical Foundations of Computer Science (MFCS 2026) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.MFCS.2026.5 urn:nbn:de:0030-drops-273867 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2026.5 eng https://creativecommons.org/licenses/by/4.0/legalcode