FYI, Reiko On 06/12/2021, 08:37, "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 December 10, 15:00 CET "Formalizing Category Theory using Type Theory: A Discussion", E.J. Gallego Arias (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 December 10, 2021, 15:00 CET Title: Formalizing Category Theory using Type Theory: A Discussion Speaker: Emilio Jesús Gallego Arias (Université de Paris, CNRS, IRIF, France) Abstract: Since its inception at the start of the 20th century, type theory has become a core foundational tool for those interested in the logical foundations of mathematics and computer science. A key milestone on the field is the Calculus of Inductive Constructions, the type theory that lies at the heart of modern interactive proof assistants such as Coq or Lean. The CiC is remarkably expressive, yet remains computationally tractable, leading to important milestones in computer-checked mathematical results such as the 4 color theorem or the Feit-Thompson theorem. In this talk, we will present the calculus of inductive constructions as currently implemented in the Coq proof assistant, and we will explore the encoding of basic constructions of category theory in Coq, placing a particular emphasis the usability and modularity of our definitions. Zoom registration link: https://u-paris.zoom.us/meeting/register/tZwrdO2hrDssHtEB5TYi6tZPmm2hn1QCrsp... Link to YouTube live stream: https://youtu.be/lM0b3oHDunU ___________________________________________________ ---------------------------------------------------------------------------- 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/ ]