In the setting of process algebras (CCS; pi-calculus; etc.), linear logic gave a substantial contribution to the extension of the Curry-Howard isomorphism to such calculi, used to model concurrent systems. The focus of this work is the multiplicative fragment of CCS, which simpli_es the problem, and thus the solutions, which can be later extended to the full calculus.
The main issue is to preserve the non-determinism of the calculus. By a direct typing in linear logic, this non determinism is lost, due to the confluent nature of cut elimination - only one of the possible outcomes can be kept. Type systems based on linear logic de_ne a correspondence between CCS terms - or executions of a term - and LL proof-nets, often imposing determinism in execution either by restricting the process to functional behaviour, or typing only a part of all the possible execution paths.
In this work we de_ne a translation of MCCS into Ludics, in order to obtain a type able to describe all the execution paths and thus the process itself. Due to the interactive nature of its objects, the designs, ludics seems the right setting to de_ne a correspondence between interaction (the equivalent of cut elimination) and execution. Behaviours, sets of designs closed by bi-orthogonality, are used to type MCCS terms. Exploiting particular noncommutative designs we impose restrictions on behaviours, in order to rule out the interactions not corresponding to possible execution on the translated MCCS term. Indeed, since some execution steps do not commute, a partial order is de_nable on execution; non commutativity in ludics is used to match this partial order, allowing in the behaviour only the designs whose interaction, with its orthogonal, do correspond to possible execution paths.
In this way we obtain a one to one correspondence between interaction and execution: for each execution path on the term there is a corresponding interaction of the behaviour with its orthogonal, and vice versa, preserving non-determinism to some extent.