Towards an embedding of Graph Transformation in Intuitionistic Linear Logic

Paolo Torrini
(University of Leicester)
Reiko Heckel
(University of Leicester)

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.

In Filippo Bonchi, Davide Grohmann, Paola Spoletini and Emilio Tuosto: Proceedings 2nd Interaction and Concurrency Experience Structured Interactions (ICE 2009), Bologna, Italy, 31st August 2009, Electronic Proceedings in Theoretical Computer Science 12, pp. 99–115.
Published: 3rd December 2009.

ArXived at: bibtex PDF

Comments and questions to:
For website issues: