categories - Category Theory list
 help / color / mirror / Atom feed
* FW: Invitation: GReTA-ExACT online workgroup, Friday December 10, 2021, 15:00 CET
@ 2021-12-06 10:54 Reiko Heckel
  0 siblings, 0 replies; only message in thread
From: Reiko Heckel @ 2021-12-06 10:54 UTC (permalink / raw)
  To: gratra, categories

FYI, Reiko

On 06/12/2021, 08:37, "GReTA Seminar organisers" <> 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 (, 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 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


Emilio Jesús Gallego Arias (Université de Paris, CNRS, IRIF, France)


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:

Link to YouTube live stream:


GReTA - Graph TRansformation Theory and Applications
                 International Online Seminar Series

[For admin and other information see: ]

^ permalink raw reply	[flat|nested] only message in thread

only message in thread, other threads:[~2021-12-06 10:54 UTC | newest]

Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2021-12-06 10:54 FW: Invitation: GReTA-ExACT online workgroup, Friday December 10, 2021, 15:00 CET Reiko Heckel

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox