Towards an embedding of Graph Transformation in Intuitionistic Linear Logic

TL;DR

This paper presents a novel embedding of graph transformation systems into quantified linear logic, establishing a Curry-Howard isomorphism that enables encoding and reasoning about graph transformations within a logical framework.

Contribution

It introduces a new embedding of double-pushout graph transformations into linear logic, linking graph rewriting to proof theory and enabling formal reasoning about graph transformations.

Findings

Establishes a Curry-Howard isomorphism between graphs and proofs.

Provides a logical language to encode and analyze graph transformations.

Demonstrates the potential for formal reasoning about graph rewriting systems.

Abstract

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.