Recent advances in applied category theory and the maturation of proof assistants such as Rocq [1](formerly Coq), Isabelle/HOL, and Lean have opened new frontiers for formalizing complex mathematical structures. Among these, the algebraic approach to graph rewriting—rooted in rich categorical foundations—offers a compelling case for mechanized reasoning.
This talk presents recent progress on developing a Rocq-based interactive framework for certifying proofs in graph transformation theory. Central to this work is the Instantiation Calculus, a novel formalism developed within the ANR CoREACT project [2], which leverages a particular kind of hyperdoctrines to rigorously encode diagrammatic proofs. We will illustrate how this calculus supports the formalization of essential reasoning patterns in theoretical graph transformation, while also highlighting avenues for its broader application in graph rewriting theory.
