A special treat this week, making executable category theory work for graph transformation. Reiko On 01/11/2021, 09:45, "GReTA Seminar organisers" <greta@irif.fr> wrote: Dear colleagues, It is our great pleasure to invite you to the next seminar of the “GReTA - Graph Transformation Theory and Applications” series: Friday November 5, 15:00 CET "GReTA-ExACT: towards Executable Applied Category Theory", N. Behr (abstract, Zoom and YouTube links attached below) The GReTA seminar series aims to serve as a platform for the international graph rewriting community, to promote recent developments and trends in the field, and to permit a regular networking and interaction between members of this community. Seminars are scheduled twice a month (cf. https://www.irif.fr/~greta/#talks for a list of upcoming events). With best regards, Nicolas Behr, Andrea Corradini, Jean Krivine and Reiko Heckel (GReTA organisers) ___________________________________________________ Date and time: Friday November 5, 2021, 15:00 CET Title: GReTA-ExACT: towards Executable Applied Category Theory Speaker: Nicolas Behr (Université de Paris, CNRS, IRIF, France) 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 Zoom registration link: https://u-paris.zoom.us/meeting/register/tZwrcuGoqT4qGd1HCZQnhptpmt0aTiWdDF6... Link to YouTube live stream: https://youtu.be/tx0asw82EXU ___________________________________________________ ---------------------------------------------------------------------------- GReTA - Graph TRansformation Theory and Applications International Online Seminar Series ---------------------------------------------------------------------------- Contact: greta@irif.fr Webpage: www.irif.fr/~greta<http://www.irif.fr/~greta> YouTube: https://www.youtube.com/channel/UC6j-G6oPmkqCgOx6UQOUhSQ Twitter: https://twitter.com/GReTAseminars [For admin and other information see: http://www.mta.ca/~cat-dist/ ]