Complete Realisation of Choreographies and Multi-party Session Types

Complete realisation of choreographies has been largely neglected in the context of multiparty session types, in which realisation is generally understood as partial. We introduce the notion of whole-spectrum realisation according to which the deterministic implementation of a role of a choreography cannot persistently avoid the execution of a branch of an internal choice specified by that choreography. Although whole-spectrum realisation is defined as a relation between the execution traces of a global type and those of its candidate implementations, it can be checked by using multiparty session types. We represent choreographies as minor variants of the global types of Carbone, Honda, and Yoshida and use local types projections to validate processes in a type system that guarantees whole-spectrum realisability.