Concurrency from ℕ-linearity

I will introduce the resource calculus, a diagrammatic language for concurrency. Significantly, it uses the same syntax as graphical linear algebra—an algebraic formalism used to reason compositionally about R-linear systems for some choice of semiring R. When R is a field, its semantics and equational theory are well understood. In this setting, graphical linear algebra generalises signal flow graphs, another language commonly used in control theory to specify and reason about the behaviour of linear dynamical systems. Our approach to concurrency stems from the simple but fruitful observation that, by taking R = ℕ, we obtain an algebra of connectors that manipulate discrete resources, for which concurrent behaviour patterns emerge. When endowed with state, the resulting language allows us to specify a broad class of distributed systems, sufficiently expressive to encode Petri nets and reason about their behaviour in a modular way. If time allows, we will also study the affine extension of this language and showcase its expressiveness using other examples from concurrency theory. This is joint work with Filippo Bonchi, Pawel Sobocinski and Fabio Zanasi.