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 -