Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2504.21108 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866915891948552192 |
|---|---|
| author | Prokić, Ivan Prokić, Simona Ghilezan, Silvia Scalas, Alceste Yoshida, Nobuko |
| author_facet | Prokić, Ivan Prokić, Simona Ghilezan, Silvia Scalas, Alceste Yoshida, Nobuko |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2504_21108 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | On Asynchronous Multiparty Session Types for Federated Learning Prokić, Ivan Prokić, Simona Ghilezan, Silvia Scalas, Alceste Yoshida, Nobuko Logic in Computer Science 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. |
| title | On Asynchronous Multiparty Session Types for Federated Learning |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2504.21108 |