Graph transformation and intuitionistic linear logic

Graph transformation has been used in the model-driven development of object-oriented programs as well as in the modelling of concurrent systems. The application of a transformation rule can be characterised algebraically as a construction of a double-pushout diagram in the category of graphs. We show how intuitionistic linear logic with proof terms can be extended with resource-bound quantification, allowing for an implicit handling of the double-pushout conditions, and how resource logic can be used to reason about reachability in graph transformation systems