Coq-based Rewriting: Towards Executable Applied Category Theory


Consortium: IRIF (Université Paris Cité), LIP (ENS-Lyon), LIX (École Polytechnique), Sophia-Antipolis (Inria)

Meet the team →     Open positions →     @anrcoreact on Twitter/X →

Coq-based Rewriting:
Towards Executable 
Applied Category Theory

Events

Date Time (Europe/Paris) Location Details
21/05/2024 13:00 - 15:00 IRIF - Université Paris Cité N. van der Weide: Formalization of Double-Categores in UniMath (research talk)
11/03/2024 - 13/03/2024 LIP - ENS Lyon CoREACT general meeting
20/11/2023 13:00 - 17:00 IRIF - Université Paris Cité CoREACT general meeting
12/10/2023 14:00 - 16:00 IRIF - Université Paris Cité A. Burroni: Algèbre Graphiques (research talk)
19/04/2023 08:30 - 18:30 IRIF - Université Paris Cité CoREACT kick-off meeting

Overview

The recent advent of applied category theory (ACT) and large-scale projects to formalise mathematics using proof assistants such as Coq, Isabelle/HOL, or Lean have opened up promising research avenues at the crossroads of several theoretical disciplines. We propose to combine these paradigms in a field of research in theoretical computer science that lends itself ideally to it: the theory of compositional categorical rewriting, a modern generalisation of the algebraic approach to graph rewriting.

Starting from the pioneering work of Ehrig et al. in the early 1970s, with as a key milestone the introduction of the theory of adhesive categories introduced by Lack and Sobocinski in the early 2000s, the categorical rewriting approach allows to deal with a wide variety of systems of practical and theoretical interest, and has de facto imposed itself as the standard approach in the field.

A peculiarity of categorical rewriting lies in the nature of lemmata and proofs in this formalism, which make intensive use of commutative diagrams and a diagrammatic calculus on them. This naturally motivates the development of an appropriate approach to exploit this type of highly modularised mathematical reasoning within formal developments in Coq and explore the possibility of interacting with Coq in diagrammatic form.

One of the main goals of this project is to bring together a team of experts in the field and an international online interest group to develop and maintain an interactive Coq-based wiki system for categorical rewriting theory, aimed at both certifying and preserving knowledge in this area of research in a modern and freely accessible format.