On Asynchronous Multiparty Session Types for Federated Learning
This work addresses verification challenges for federated learning systems, offering incremental improvements to session typing theory.
The paper tackles the problem of modeling and verifying federated learning protocols by extending asynchronous multiparty session types to support multi-participant input/output operations and introducing a tailored subtyping relation for safe process replacements, with formal proofs of safety, deadlock-freedom, liveness, and session fidelity.
This paper improves the session typing theory to support the modelling and verification of processes that implement federated learning protocols. To this end, we build upon the asynchronous ``bottom-up'' session typing approach by adding support for input/output operations directed towards multiple participants at the same time. We further enhance the flexibility of our typing discipline and allow for safe process replacements by introducing a session subtyping relation tailored for this setting. We formally prove safety, deadlock-freedom, liveness, and session fidelity properties for our session typing system. Moreover, we highlight the nuances of our session typing system, which (compared to previous work) reveals interesting interplays and trade-offs between safety, liveness, and the flexibility of the subtyping relation.