From Petri nets to linear logic

Narciso Martí-Oliet, José Meseguer

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.

Original languageEnglish (US)
Title of host publicationCategory Theory and Computer Science - Proceedings
EditorsDavid E. Rydeheard, Axel Poigne, Andrew M. Pitts, David H. Pitt, Peter Dybjer
Number of pages28
ISBN (Print)9783540516620
StatePublished - 1989
Externally publishedYes
Event3rd International Conference on Category Theory and Computer Science, CTCS 1989 - Manchester, United Kingdom
Duration: Sep 5 1989Sep 8 1989

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume389 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other3rd International Conference on Category Theory and Computer Science, CTCS 1989
Country/TerritoryUnited Kingdom

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'From Petri nets to linear logic'. Together they form a unique fingerprint.

Cite this