From Petri nets to linear logic
- 4 March 1991
- journal article
- research article
- Published by Cambridge University Press (CUP) in Mathematical Structures in Computer Science
- Vol. 1 (1), 69-101
- https://doi.org/10.1017/s0960129500000062
Abstract
Linear logic has recently been introduced by Girard as a logic of actions that seems well suited for concurrent computation. In this paper, we establish a systematic correspondence between Petri nets, linear logic theories, and linear categories. Such a correspondence sheds new light on the relationships between linear logic and concurrency, and on how both areas are related to category theory. Categories are here viewed as concurrent systems the objects of which are states, and the morphisms of which are transitions. This is an instance of the Lambek-Lawvere correspondence between logic and category theory that cannot be expressed within the more restricted framework of the Curry-Howard correspondence.Keywords
This publication has 15 references indexed in Scilit:
- Petri nets are monoidsInformation and Computation, 1990
- Quantales and (noncommutative) linear logicThe Journal of Symbolic Logic, 1990
- Linear logic, *-autonomous categories and cofree coalgebrasContemporary Mathematics, 1989
- The Dialectica categoriesContemporary Mathematics, 1989
- The linear abstract machineTheoretical Computer Science, 1988
- Linear logicTheoretical Computer Science, 1987
- System modelling with high-level Petri netsTheoretical Computer Science, 1981
- Adjointness in FoundationsDialectica, 1969
- Deductive systems and categories II. Standard constructions and closed categoriesLecture Notes in Mathematics, 1969
- Deductive systems and categoriesTheory of Computing Systems, 1968