Towards an Embedding of Graph Transformation in Intuitionistic Linear Logic

Linear logics have been shown to be able to embed both rewriting-based approaches and process calculi in a single, declarative framework. In this paper we are exploring the embedding of double-pushout graph transformations into quantified linear logic, leading to a Curry-Howard style isomorphism between graphs / transformations and formulas / proof terms. With linear implication representing rules and reachability of graphs, and the tensor modelling parallel composition of graphs / transformations, we obtain a language able to encode graph transformation systems and their computations as well as reason about their properties.