Multiparty Session Types Within a Canonical Binary Theory, and Beyond

A widespread approach to software service analysis uses session types. Very different type theories for binary and multiparty protocols have been developed; stablishing precise connections between them remains an open problem. In this talk, I will present the first formal relation between two existing theories of binary and multiparty session types: a binary system rooted in linear logic, and a multiparty system based on automata theory. Our results enable the analysis of multiparty protocols using a (much simpler) type theory for binary protocols, ensuring protocol fidelity and deadlock-freedom.