| Summary: | Multiparty session types (MP) are a type discipline for enforcing
the structured, deadlock-free communication of concurrent and
message-passing programs. Traditional MP have a limited form
of choice in which alternative communication possibilities are offered by a single participant and selected by another. Mixed choice
multiparty session types (MCMP) extend the choice construct to include both selections and offers in the same choice. This paper first
proposes a general typing system for a mixed choice synchronous
multiparty session calculus, and prove type soundness, communication safety, and deadlock-freedom.
Next we compare expressiveness of nine subcalcli of MCMPcalculus by examining their encodability (there exists a good encoding from one to another) and separation (there exists no good
encoding from one calculus to another). We prove 8 new encodablity results and 20 new separation results. In summary, MCMP
is strictly more expressive than classical multiparty sessions (MP)
in [19] and mixed choice in mixed sessions in [8]. This contrasts
to the results proven in [8, 50] where mixed sessions [8] do not
add any expressiveness to non-mixed fundamental sessions in [64],
shedding a light on expressiveness of multiparty mixed choice.
|
|---|