Una interpretazione di CCS nella ludica

Stefano Del Vecchio (Università Roma Tre - Université Paris Nord)
24/11/2017 - 11:00
Dipartimento di Matematica e Fisica, Palazzina C, Aula 311

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 Ludics as the target system. Indeed interaction, Ludics' dynamic, allows to fully represent both the non-determinism and non-confluence of the calculus. CCS processes are interpreted into carefully defined behaviours of Ludics using a new construction, called directed behaviour, that allows controlled interaction paths by using pruned designs. Execution of processes is characterized 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 deadlock-free ones.