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 and transformations on one hand, formulas and
proof terms on the other. With linear implication representing rules and reachability of graphs, and the
tensor modelling parallel composition of graphs and transformations, we obtain a language
able to encode graph transformation systems and their computations as well as reason about
their properties.
|