TY - GEN

T1 - From Petri nets to linear logic

AU - Martí-Oliet, Narciso

AU - Meseguer, José

N1 - Funding Information:
Since for many categories the morphisms are functions, and for the particular case of typed lambda calculi the associated categories were cartesian closed categories, this less well-known correspondence has to a large extent passed unnoticed as yet another variant of the Curry-Howard correspondence in categorical garb. The crucial point being ignored, though, is that category theory is an abstract theory of mathematical structures and that, therefore, morphisms in a category are not functions in general, although they can happen to be functions in particular categories. An inspection of the original papers by Lambek and Lawvere makes absolutely clear *Supported by Office of Naval Research Contracts N00014-86-C-0450 and N00014-88-C-0618, NSF Grant CCR-8707155, and a grant from the System Development Foundation. The first author is supported by a Research Fellowship of the Spanish Ministry for Education and Science.

PY - 1989

Y1 - 1989

N2 - Linear logic has been recently 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 whose objects are states, and whose morphisms 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.

AB - Linear logic has been recently 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 whose objects are states, and whose morphisms 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.

UR - http://www.scopus.com/inward/record.url?scp=84973979829&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84973979829&partnerID=8YFLogxK

U2 - 10.1007/BFb0018359

DO - 10.1007/BFb0018359

M3 - Conference contribution

AN - SCOPUS:84973979829

SN - 9783540516620

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 313

EP - 340

BT - Category Theory and Computer Science - Proceedings

A2 - Rydeheard, David E.

A2 - Poigne, Axel

A2 - Pitts, Andrew M.

A2 - Pitt, David H.

A2 - Dybjer, Peter

PB - Springer

T2 - 3rd International Conference on Category Theory and Computer Science, CTCS 1989

Y2 - 5 September 1989 through 8 September 1989

ER -