Ludics is a Model for the Finitary Linear Pi-Calculus

We analyze in game-semantical terms the finitary fragment of the linear π-calculus. This calculus was introduced by Yoshida, Honda, and Berger, and then refined by Honda and Laurent. The features of this calculus - asynchrony and locality in particular - have a precise correspondence in Game Semantics. Building on work by Varacca and Yoshida, we interpret π-processes in linear strategies, that is the strategies introduced by Girard within the setting of Ludics. We prove that the model is fully complete and fully abstract w.r.t. the calculus.