Document Open Access Logo

Diagrammatic Reasoning, Formally (Invited Talk)

Author Damien Pous

PDF

File

Thumbnail PDF
PDF
LIPIcs.MFCS.2026.5.pdf
  • Filesize: 377 kB
  • 1 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
Keywords
  • Formal proofs
  • graphical proofs
  • string diagrams
  • monoidal categories
  • Kleene algebra
  • relation algebra
  • Rocq

Metrics

Abstract

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].

Cite As Get BibTex

Damien Pous. Diagrammatic Reasoning, Formally (Invited Talk). In 51st International Symposium on Mathematical Foundations of Computer Science (MFCS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 386, p. 5:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.MFCS.2026.5

Author Details

Damien Pous
  • CNRS, LIP, ENS de Lyon, France

Supplementary Materials

References

  1. André Joyal and Ross Street. The geometry of tensor calculus, I. Advances in Mathematics, 88:55-112, 1991. URL: https://doi.org/10.1016/0001-8708(91)90003-P.
  2. Dexter Kozen. Kleene algebra with tests. ACM Trans. Program. Lang. Syst., 19(3):427-443, May 1997. URL: https://doi.org/10.1145/256167.256195.
  3. Damien Pous. Kleene Algebra with Tests and Coq tools for while programs. In Proc. ITP'13, volume 7998 of LNCS, pages 180-196. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39634-2_15.
  4. Damien Pous. String diagrams for monoidal categories, in rocq. In Ekaterina Komendantskaya and Tobias Nipkow, editors, Proc. ITP'26, volume 382, pages 28:1-28:20. LIPIcs, 2026. URL: https://doi.org/10.4230/LIPIcs.ITP.2026.28.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact