The central aims of this workgroup consist in providing an interdisciplinary forum for exploring the diverse aspects of applied category theory relevant in graph transformation systems and their generalizations, in developing a methodology for formalizing diagrammatic proofs as relevant in rewriting theories via proof assistants such as Coq, and in establishing a community-driven wiki system and repository for mathematical knowledge in our research field (akin to a domain-specific Coq-enabled variant of the nLab). A further research question will explore the possibility of deriving reference prototype implementations of concrete rewriting systems (e.g., over multi- or simple directed graphs) directly from the category-theoretical semantics, in the spirit of the translation-based approaches (utilizing theorem provers such as Microsoft Z3).

  • To receive regular updates on the GReTA ExACT workgroup sessions, please consider subscribing to our mailing list.
  • To suggest speakers and topics for upcoming sessions, and for any other form of feedback and discussions, please consider joining the GReTA ExACT Mattermost channel.

Upcoming Sessions

Previous Sessions

SMTCoq: the power of SMT solving in Coq

SMTCoq is a tool to make the Coq proof assistant and SMT solvers cooperate, with the same degree of confidence as Coq. In this talk, I will give an overview of its potential:

  • checking SMT answers, both in Coq and externally using the Coq extraction mechanism
  • importing SMT problems as Coq theorems
  • calling SMT solvers to ease Coq proof building, in a ongoing project called Sniper.

An API to build first-order SMTCoq terms and formulas is also under progress, in order to have an easy access to …

A categorical diagram editor to help formalising commutation proofs
I will present a categorical diagram editor ( implemented in Elm that generates Coq proof scripts (based on the UniMath library), letting the user prove manually commutation of each subdiagram. Conversely, the editor can parse a Coq goal stating equality between two composition of morphisms and generate a diagram out of it.