Resource-Bound Quantification for Graph Transformation

Paolo Torrini
Reiko Heckel

Graph transformation has been used to model concurrent systems in software engineering, as well as in biochemistry and life sciences. The application of a transformation rule can be characterised algebraically as construction of a double-pushout (DPO) diagram in the category of graphs. We show how intuitionistic linear logic can be extended with resource-bound quantification, allowing for an implicit handling of the DPO conditions, and how resource logic can be used to reason about graph transformation systems.

In Mário Florido and Ian Mackie: Proceedings First International Workshop on Linearity (LINEARITY 2009), Coimbra, Portugal, 12th September 2009, Electronic Proceedings in Theoretical Computer Science 22, pp. 14–25.
Published: 30th March 2010.

ArXived at: http://dx.doi.org/10.4204/EPTCS.22.2 bibtex PDF

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org