From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/10614 Path: news.gmane.io!.POSTED.blaine.gmane.org!not-for-mail From: Reiko Heckel Newsgroups: gmane.science.mathematics.categories Subject: FW: Invitation: GReTA-ExACT online workgroup, Friday November 26, 2021, 15:00 CET Date: Mon, 22 Nov 2021 15:20:17 +0000 Message-ID: Reply-To: Reiko Heckel Mime-Version: 1.0 Content-Type: text/plain; charset="Windows-1252" Content-Transfer-Encoding: quoted-printable Injection-Info: ciao.gmane.io; posting-host="blaine.gmane.org:116.202.254.214"; logging-data="12935"; mail-complaints-to="usenet@ciao.gmane.io" To: "gratra@upb.de" , "categories@mta.ca" Original-X-From: majordomo@rr.mta.ca Tue Nov 23 21:51:26 2021 Return-path: Envelope-to: gsmc-categories@m.gmane-mx.org Original-Received: from smtp2.mta.ca ([198.164.44.75]) by ciao.gmane.io with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.92) (envelope-from ) id 1mpclC-0003Cc-1z for gsmc-categories@m.gmane-mx.org; Tue, 23 Nov 2021 21:51:26 +0100 Original-Received: from rr.mta.ca ([198.164.44.159]:36504) by smtp2.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1mpclE-0006n5-F3; Tue, 23 Nov 2021 16:51:28 -0400 Original-Received: from majordomo by rr.mta.ca with local (Exim 4.92.1) (envelope-from ) id 1mpckF-00046T-87 for categories-list@rr.mta.ca; Tue, 23 Nov 2021 16:50:27 -0400 Accept-Language: en-GB, en-US Content-Language: en-GB Precedence: bulk Xref: news.gmane.io gmane.science.mathematics.categories:10614 Archived-At: Graph transformation meets executable applied CT! Reiko On 22/11/2021, 07:39, "GReTA Seminar organisers" wrote: Dear colleagues, It is our great pleasure to invite you to the next session of the =93GReTA-= ExACT - Executable Applied Category Theory=94 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 G= ReTA ExACT (Executable Applied Category Theory) online workgroup aims at pr= oviding an interdisciplinary forum for exploring the diverse aspects of app= lied category theory relevant in graph transformation systems and their gen= eralizations, in developing a methodology for formalizing diagrammatic proo= fs as relevant in rewriting theories via proof assistants such as Coq, and = in establishing a community-driven wiki system and repository for mathemati= cal 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 concre= te 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 (includ= ing 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=E9diterran=E9e, Sophia-Antipolis, Fra= nce) Abstract: Libraries of machine checked code are, nowadays, organized around hierarchi= es of algebraic structures. Unfortunately the language of Type Theory and t= he 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 be= tween using type classes and canonical structures for inference. To this, o= ne 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 p= rovides the final user linguistic constructs to build instances (examples) = of structures and to teach the elaborator of Coq how to take advantage of t= his knowledge during type inference. Finally HB lets the library designer i= mprove 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-GgpjMtEtXUIhbc0Adinn7RXAqZbg= H4 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 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/ ]