Fundamentals of compositional rewriting theory
From MaRDI portal
Publication:6052944
Abstract: A foundational theory of compositional categorical rewriting theory is presented, based on a collection of fibration-like properties that collectively induce and structure intrinsically the large collection of lemmata used in the proofs of theorems such as concurrency and associativity. The resulting highly generic proofs of these theorems are given; it is noteworthy that the proof of the concurrency theorem takes only a few lines and, while that of associativity remains somewhat longer, it would be unreadably long if written directly in terms of the basic lemmata. In addition to improving, or even enabling, the readability of human-written proofs, we anticipate that this more generic and modular style of writing proofs should organize and inform the production of formalized proofs in a proof assistant such as Coq or Isabelle. A curated list of known instances of our framework is used to conclude the paper with a detailed discussion of the conditions under which the Double Pushout and Sesqui-Pushout semantics of graph transformation are compositional.
Cites work
- 2-Dimensional Categories
- M, N-adhesive transformation systems
- A software package for chemically inspired graph transformation
- Abstract and concrete categories: the joy of cats
- Adhesive and quasiadhesive categories
- AGREE -- algebraic graph rewriting with controlled embedding
- Algebraic approach to single-pushout graph transformation
- Categorical frameworks for graph transformation and HLR systems based on the DPO approach
- Categorical logic and type theory
- Compositionality of rewriting rules with conditions
- Concurrency theorems for non-linear rewriting theories
- Concurrent Separation Logic Meets Template Games
- Distributed graphs and graph transformation
- Exponentiable morphisms, partial products and pullback complements
- Fibered categories and the foundations of naive category theory
- Finitary \(\mathcal{M}\)-adhesive categories
- Foundations of Software Science and Computation Structures
- Fundamentals of algebraic graph transformation
- Graph rewriting and relabeling with PBPO\textsuperscript{+}
- Graph Transformations
- Handbook of Graph Grammars and Computing by Graph Transformation
- Hereditary pushouts reconsidered
- Hierarchical Graph Transformation Revisited
- How to delete categorically -- two pushout complement constructions
- scientific article; zbMATH DE number 3667032 (Why is no real title available?)
- scientific article; zbMATH DE number 3522194 (Why is no real title available?)
- scientific article; zbMATH DE number 692330 (Why is no real title available?)
- scientific article; zbMATH DE number 1840601 (Why is no real title available?)
- scientific article; zbMATH DE number 1389226 (Why is no real title available?)
- scientific article; zbMATH DE number 7453087 (Why is no real title available?)
- scientific article; zbMATH DE number 7453970 (Why is no real title available?)
- scientific article; zbMATH DE number 7456055 (Why is no real title available?)
- scientific article; zbMATH DE number 7456060 (Why is no real title available?)
- scientific article; zbMATH DE number 7725598 (Why is no real title available?)
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Isabelle/HOL. A proof assistant for higher-order logic
- Monads in double categories
- Multi-amalgamation of rules with application conditions in \(\mathcal{M}\)-adhesive categories
- On term graphs as an adhesive category
- On the axioms for adhesive and quasiadhesive categories
- On the essence and initiality of conflicts in \(\mathcal{M} \)-adhesive transformation systems
- Polymorphic sesqui-pushout graph rewriting
- Pseudo algebras and pseudo double categories
- Quasitopoi, logic and Heyting-valued models
- Quasitoposes, Quasiadhesive Categories and Artin Glueing
- Restriction categories II: Partial map classification
- Restriction categories. I: Categories of partial maps
- Reversible sesqui-pushout rewriting
- Rewriting theory for the life sciences: a unifying theory of CTMC semantics
- Rule algebras for adhesive categories
- Rule-Based Modelling of Cellular Signalling
- Sesqui-Pushout Rewriting
- The Lean theorem prover (system description)
- The PBPO graph transformation approach
- Thermodynamic graph-rewriting
- Toposes Are Adhesive
Cited in
(10)- Composing dinatural transformations: towards a calculus of substitution
- Theory and practice of second-order rewriting: foundation, evolution, and SOL
- Specification and modelling of computing systems through graphs and graph transformation
- A simple criterion for \(\mathcal{M}, \mathcal{N}\)-adhesivity
- A living monograph for graph transformation
- Diagrammatic calculus and generalized associativity for higher-arity tensor operations
- A theory of binding structures and applications to rewriting
- Left-linear rewriting in adhesive categories
- Termination of graph transformation systems using weighted subgraph counting
- Insights from univalent foundations: a case study using double categories
This page was built for publication: Fundamentals of compositional rewriting theory
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6052944)
