What is a Good Projection?: Correctness and Separation Results of End-Point Projections

Jake Masters, Nobuko Yoshida

\emph{Multiparty session types} (MPST) is a type discipline for ensuring distributed programs are implemented correctly \emph{by construction}. MPST starts by specifying a choreographic protocol as a \emph{global type} and \emph{projects} it onto each participant, generating \emph{local types} with a guarantee of type soundness and deadlock-freedom. A central issue of MPST is that its type soundness is fragile, as it must be proven each time with respect to a chosen projection algorithm under specific semantics with a specific program correctness goal. To overcome this problem, we propose general criteria for a \emph{good projection} -- a set of requirements for projection algorithms by which type soundness, deadlock-freedom and liveness of distributed programs are \emph{automatically} derived. Using the criteria, we prove that 8 distinct projections in the literature are good under both synchronous and asynchronous semantics, and that 4 are incorrect, failing type soundness. We extend the good projection criteria to mixed choice global types and asynchronous communication optimisations, proposing new ``good projection'' algorithms. We apply properties of good projections to…