Coq-based Rewriting: towards Executable Applied Category Theory – CoREACT

The recent advent of applied category theory (ACT) and large-scale projects to formalize 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 generalization 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 modularized 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.