Towards an embedding of Graph Transformation in Intuitionistic Linear Logic
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 bet...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2009-12-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/0911.5525v1 |
| _version_ | 1818514045736583168 |
|---|---|
| author | Reiko Heckel Paolo Torrini |
| author_facet | Reiko Heckel Paolo Torrini |
| author_sort | Reiko Heckel |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-12-11T00:09:51Z |
| format | Article |
| id | doaj.art-bbbb67dbd77c443cb5c2f15d42d3bdcd |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-12-11T00:09:51Z |
| publishDate | 2009-12-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-bbbb67dbd77c443cb5c2f15d42d3bdcd2022-12-22T01:28:11ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802009-12-0112Proc. ICE 20099911510.4204/EPTCS.12.7Towards an embedding of Graph Transformation in Intuitionistic Linear LogicReiko HeckelPaolo TorriniLinear 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.http://arxiv.org/pdf/0911.5525v1 |
| spellingShingle | Reiko Heckel Paolo Torrini Towards an embedding of Graph Transformation in Intuitionistic Linear Logic Electronic Proceedings in Theoretical Computer Science |
| title | Towards an embedding of Graph Transformation in Intuitionistic Linear Logic |
| title_full | Towards an embedding of Graph Transformation in Intuitionistic Linear Logic |
| title_fullStr | Towards an embedding of Graph Transformation in Intuitionistic Linear Logic |
| title_full_unstemmed | Towards an embedding of Graph Transformation in Intuitionistic Linear Logic |
| title_short | Towards an embedding of Graph Transformation in Intuitionistic Linear Logic |
| title_sort | towards an embedding of graph transformation in intuitionistic linear logic |
| url | http://arxiv.org/pdf/0911.5525v1 |
| work_keys_str_mv | AT reikoheckel towardsanembeddingofgraphtransformationinintuitionisticlinearlogic AT paolotorrini towardsanembeddingofgraphtransformationinintuitionisticlinearlogic |