Graph transformation meets executable applied CT! Reiko On 22/11/2021, 07:39, "GReTA Seminar organisers" <greta@irif.fr> wrote: Dear colleagues, It is our great pleasure to invite you to the next session of the “GReTA-ExACT - Executable Applied Category Theory” online workgroup: Friday November 26, 10:00 CET "Hierarchy Builder", C. Cohen (abstract, Zoom and YouTube links attached below) In the context of the GReTA - "Graph TRansformation Theory and Applications" online seminar series hosted at IRIF (https://www.irif.fr/~greta/), the GReTA ExACT (Executable Applied Category Theory) online workgroup aims at 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 (utilizing theorem provers such as Microsoft Z3). Please refer to https://www.irif.fr/~greta/gretaexact/ for further details (including information on how to register for participating in the Zoom meetings). With best regards, Nicolas Behr, Andrea Corradini, Jean Krivine and Reiko Heckel (GReTA organisers) ___________________________________________________ Date and time: Friday November 26, 2021, 15:00 CET Title: Hierarchy Builder Speaker: Cyril Cohen (Inria Sophia-Antipolis Méditerranée, Sophia-Antipolis, France) Abstract: Libraries of machine checked code are, nowadays, organized around hierarchies of algebraic structures. Unfortunately the language of Type Theory and the features provided by the Coq system make the construction of a hierarchy hard even for expert users. The difficulty begins with the non-orthogonal choices, between storing information as record fields or parameters, and between using type classes and canonical structures for inference. To this, one may add the concerns about performance and about the usability, by a non expert, of the final hierarchy. HB gives the library designer a language to describe the building blocks of algebraic structures and to assemble them into a hierarchy. Similarly it provides the final user linguistic constructs to build instances (examples) of structures and to teach the elaborator of Coq how to take advantage of this knowledge during type inference. Finally HB lets the library designer improve the usability of his library by providing alternative interfaces to the primitive ones, a feature that can also be used to accommodate changes to the hierarchy without breaking user code. This is a joint work with Kazuhiko Sakaguchi and Enrico Tassi. Zoom registration link: https://u-paris.zoom.us/meeting/register/tZIqd-GgpjMtEtXUIhbc0Adinn7RXAqZbgH... Link to YouTube live stream: https://youtu.be/nMynSM9Xnkw ___________________________________________________ ---------------------------------------------------------------------------- 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/ ]