π-calculus, Session Types research at the University of Oxford
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 of- fered by a single participant and selected by another. Mixed choice multiparty session types (MCMP) extend the choice construct to in- clude 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, communi- cation safety, and deadlock-freedom. Next we compare expressiveness of nine subcalcli of MCMP - calculus by examining their encodability (there exists a good en- coding from one to another) and separation (there exists no good encoding from one calculus to another). We prove 8 new encod- ablity 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, 51] where mixed sessions [8] do not add any expressiveness to non-mixed fundamental sessions in [ 65 ], shedding a light on expressiveness of multiparty mixed choice.
@article{PY2024,
author = {Kirstin Peters and Nobuko Yoshida},
title = {{Separation and Encodability in Mixed Choice Multiparty Sessions}},
journal = {LICS 2024},
pages = {--},
publisher = {ACM/IEEE},
year = 2024
}
@article{PY2024,
author = {Kirstin Peters and Nobuko Yoshida},
title = {{Separation and Encodability in Mixed Choice Multiparty Sessions}},
journal = {Logic in Computer Science},
pages = {--},
publisher = {ACM/IEEE},
year = 2024
}