PROCESS ALGEBRAS INSIDE LUDICS: AN INTERPRETATION OF THE CALCULUS OF COMMUNICATING SYSTEMS

Abstract

Starting from works aimed at extending the Curry-Howard correspondence to process calculi through linear logic, we give another Curry-Howard counterpart for Milner’s Calculus of Communicating Systems (CCS), by taking Girard’s ludics as the target system. Our aim consists in building an interpretation able to form a complete correspondence between the dynamics of the two systems. Indeed interaction, ludics’ dynamic, allows to fully represent both the non-determinism and non-confluence of the calculus. We thus give an interpretation of CCS processes into carefully defined beha viours of ludics using a new construction, called directed behaviour, that allows a controlled interaction through modified designs by the pruning technique. We characterize the execution of CCS processes as interaction on behaviours, by implicitly representing the causal order and conflict relation of Event Structures ; as a direct consequence, we are also able to interpret deadlocked processes, and identify deadlockfree ones. The final part of the thesis is dedicated to exploring the non-linear extensions of ludics, and hint at possible future developments and research directions, in order to represent processes defined by recursion