π-calculus, Session Types research at the University of Oxford
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.
@inproceedings{PPGSY2025,
author = {Ivan Prokić and Simona Prokić and Silvia Ghilezan and Alceste Scalas and Nobuko Yoshida},
title = {{On Asynchronous Multiparty Session Types for Federated Learning}},
booktitle = {22st International Colloquium on Theoretical Aspects of Computing, 2025, Marrakech, Morocco},
series = {Lecture Notes in Computer Science},
volume = {16237},
pages = {164--182},
publisher = {Springer Nature},
year = 2025
}
@inproceedings{PPGSY2025,
author = {Ivan Prokić and Simona Prokić and Silvia Ghilezan and Alceste Scalas and Nobuko Yoshida},
title = {{On Asynchronous Multiparty Session Types for Federated Learning}},
booktitle = {22st International Colloquium on Theoretical Aspects of Computing, 2025, Marrakech, Morocco},
series = {Lecture Notes in Computer Science},
volume = {16237},
pages = {164--182},
publisher = {Springer Nature},
doi = "https://doi.org/10.1007/978-3-032-11176-0_11",
year = 2025
}