Authors: Matteo Acclavio, Giovanni Bernardi, Giulia Manara and Fabrizio Montesi

The calculus of communicating systems (CCS) is a process calculus for the specification and modelling of discrete communicating systems. In this talk we define a sequent calculus operating on formulas encoding CCS processes capturing the operational semantics for the recursion-free fragment of CCS, and establish a correspondence between executions of processes and (branches of) derivations in this calculus. For this purpose, we define an extension of the first order multiplicative and additive linear logic with nominal quantifiers and a non-commutative and non-associative connective. After proving cut-elimination for this system, we show that sequent rules simulating the rules of the operational semantics of CCS are derivable our calculus. We conclude by discussing future research directions.