Generalising Projection in Asynchronous Multiparty Session Types
Rupak Majumdar, Madhavan Mukund, Felix Stutz, Damien Zufferey

TL;DR
This paper introduces a generalized projection method for multiparty session types that models complex distributed system patterns, like load balancing, by tracking message causality, thus expanding the scope of verifiable message passing protocols.
Contribution
It presents a novel, more expressive projection technique for MSTs that enables verification of systems previously incompatible with standard projections.
Findings
Allows modeling of load balancing patterns
Enables projection of more complex global types
Uses graph-theoretic techniques for soundness proof
Abstract
Multiparty session types (MSTs) provide an efficient methodology for specifying and verifying message passing software systems. In the theory of MSTs, a global type specifies the interaction among the roles at the global level. A local specification for each role is generated by projecting from the global type on to the message exchanges it participates in. Whenever a global type can be projected on to each role, the composition of the projections is deadlock free and has exactly the behaviours specified by the global type. The key to the usability of MSTs is the projection operation: a more expressive projection allows more systems to be type-checked but requires a more difficult soundness argument. In this paper, we generalise the standard projection operation in MSTs. This allows us to model and type-check many design patterns in distributed systems, such as load balancing, that are…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
