Towards Certifiable Implementation of Graph Transformation via Relation Categories

The algebraic approach to graph transformation is a general framework for the definition of transformation mechanisms for complex structures that achieves its generality by using category-theoretic abstractions.We present a framework for modular implementations of categoric graph transformation mechanisms that uses abstractions of relation categories as internal interfaces. Doing this in a dependently-typed programming language enables us to manage implementations of functionality together with their correctness proofs in the same language, thus progressing towards fully verified graph transformation system implementations.