__Abstract__*. *A seminal result in concurrency theory shows that an algebraic interpretation of Petri nets in terms of commutative monoids can be used to provide an elegant characterisation of the deterministic computations of a net via monoidal categories, accounting for their sequential and parallel composition. In turn, this characterisation leads to the interpretation of such computations as sequents of a multiplicative fragment of linear logic, thus as an instance of the classical Curry-Howard isomorphism. The talk presents a survey of the topic, including some recent results concerning non-deterministic computations, and their characterisation in terms of bimonoidal categories.