Relating Global Types and Multi-Party Sessions

Mariangiola Dezani-Ciancaglini, University of Torino, Italy

(Joint work with Giuseppe Castagna and Luca Padovani)

We present some ongoing work aimed at revisiting the theory of global types from the ground up, by first stating the properties we expect from the implementations of a given multiparty session and then studying a suitable projection algorithm enforcing these properties. We identify three fundamental properties: infinite fairness, namely the fact that the involved participants must preserve the ability to terminate successfully; absence of covert channels, which forces the participants to interact as rigorously specified in the global type; exhaustivity, ensuring that every interaction specified in the global type may take place in the implementation.