GReTA-ExACT: towards Executable Applied Category Theory
Abstract
This talk marks the beginning of GReTA-ExACT, a new online working group within the GReTA community. The aim of this working group will 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 consist in exploring the possibility for 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 as in [1],[2] (utilizing theorem provers such as Microsoft Z3).
In the first part of this talk, I will provide an illustrated tour of broad scope of mathematical concepts in modern categorical rewriting theories, ranging over the definitions of Double-Pushout (DPO) and Sesqui-Pushout (SqPO) semantics to the notions of concurrency and associativity theorems, their proofs (illustrating a particular type of diagrammatic reasoning on commutative diagrams), the theory of tracelets, their Hopf algebras and decomposition spaces, certain concepts of opfibrations and finally double-categorical structures that are currently under active investigation (joint work with Paul-André Melliès and Noam Zeilberger). In the second part of the talk, I will outline a proposal for the new GReTA-ExACT online working group format.
References:
[1] R. Heckel, L. Lambers, M.G. Saadat, “Analysis of Graph Transformation Systems: Native vs Translation-based Techniques”, EPTCS 309, 2019, pp. 1-22. http://dx.doi.org/10.4204/EPTCS.309.1
[2] N. Behr, R. Heckel, M.G. Saadat, “Efficient Computation of Graph Overlaps for Rule Composition: Theory and Z3 Prototyping”, EPTCS 330, 2020, pp. 126–144. http://dx.doi.org/10.4204/EPTCS.330.8
Nicolas Behr
CNRS Researcher in Computer Science
I am a CNRS researcher in theoretical computer science at IRIF, Université de Paris. Previously, I have been a Short-Term Fellow at CRI Paris in spring and summer of 2020, working on the development of tracelet-analysis algorithms for the biochemistry platform Kappa and for the organo-chemistry platform MØD. I previously held a Marie Skłodowska-Curie Individual Fellowship (2017-2019), working in the field of theoretical computer science at IRIF, Université Paris Diderot. The aim of my project with Jean Krivine (IRIF) consisted in developing extensions of my rule-algebraic framework to restricted variants of rewriting and to the biochemical reaction language Kappa. I am also frequently to be found at the LPTMC of the UPMC/Sorbonne/Paris 06, working with Gérard H.E. Duchamp (Paris 13) and Karol A. Penson (Paris 6) on topics in combinatorics. My previous positions include a Postdoc position with Vincent Danos at ENS Paris and at University of Edinburgh (2014-2017) and a Postdoc position in mathematical physics with Anatoly Konechny at Heriot-Watt University in Edinburgh (2011-2014).