Adhesive Category Theory for Graph Rewriting in Rocq
summary
A Rocq library implements adhesive and weaker RM and RMU adhesive category hierarchies using Hierarchy Builder and encodes morphism hierarchies (mono, reg mono, split mono, iso, adhesive morphisms). It formalizes the Church–Rosser and concurrency theorems for DPO graph rewriting, provides instances for types, finite types, simple directed graphs and presheaves, and totals about 10,000 lines (≈5k general, 2.4k adhesive theory, 400 for the two main proofs, 2k instances). Uses specific axioms (constructive indefinite description, predicate extensionality) where shown necessary and ships artifacts.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 0:30Graph rewriting with DPO
- 2:50Categorical frameworks
- 5:31Formalization challenges
- 7:45Using setoids in categories
- 8:59Hierarchies and tools
- 11:36Main theorems
- 13:33Instances and construction
- 17:30Conclusion and future work
- 19:46Q&A session
related talks
16mEnhancing universe polymorphism for Rocq: Algebraic universes, consistency checking(…)
18mCompleteness of an Axiomatization of Graph Isomorphism via Graph Rewriting in Coq
30mA Mechanised Semantics of Erlang’s References
21mNested Inductive Types for Rocq and Lean
51mElpi: rule-based meta-languge for Rocq
15mImplementing parametricity in Rocq-ELPI
23mVerifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach
22mAutomated Proof Generation for Associative and Distributive Rewriting with E-Graphs