date/vreme: 26/12/2025, 12:00
venue/mesto: TBA
Speaker / Predavač
Prof. Nobuko Yoshida, Strachey Professor of Computing, University of Oxford, UK
https://www.cs.ox.ac.uk/people/nobuko.yoshida https://mrg.cs.ox.ac.uk (home page)
Title / Naslov:
Asynchronous Global Protocols, Precisely
Abstract / Sažetak:
Joint Work with Kai Pischke and Jake Masters in University of Oxford.
Asynchronous multiparty session types are a type-based framework that ensures the compatibility of components in a distributed system by specifying a global protocol. Each component can be independently developed and refined locally, before being integrated into a larger system, leading to higher quality distributed software. This talks explains the interplay between global protocols and an asynchronous refinement relation, precise asynchronous multiparty subtyping, introduced by Ghilezan and Prokic, et al [TOCL'23].
This subtyping relation locally optimises asynchronous messaging, enabling a permutation of two actions in a component while still preserving the safety and liveness of the overall composed system. In this talk we first define the asynchronous association between a global protocol and a set of local optimised specifications. We then show the main theorems-- soundness and completeness of the operational correspondence of this asynchronous association. Finally we demonstrate that the association acts as an invariant to derive type soundness, session fidelity and liveness of the top-down system reusing the results from [TOCL'23].
We then demonstrate Federate Learning (TaRDIS use case) examples in [ECBS'25,ICTAC'25] by Prokic et al can be typed by our top-down system integrated with the asynchronous subtyping system, and implemented by Scribble with asynchronous optimisation.
About the speaker. Nobuko Yoshida is Christopher Strachey Chair of Computer Science in University of Oxford. She is an EPSRC Established Career Fellow and an Honorary Fellow at Glasgow University. Last 10 years, her main research interests are theories and applications of protocols specifications and verifications. She introduced multiparty session types [ POPL’08, JACM ] which received Most Influential POPL Paper Award in 2018 (judged by its influence over the last decade). This work enlarged the community and widened the scope of applications of session types, e.g. runtime monitoring based on Scribble (co-developed with Red Hat) has been deployed to other projects such as cyberinfrastructure in the US Ocean Observatories Initiative (OOI); and widened the scope of her research areas. She received the Test-of-time-award from PPDP'24 and the best paper awards from CC'20, COORDINATION'23 and DisCoTech'23. She received the third Suffrage Science Awards for Mathematics and Computing from MRC for her STEM activity. She is an editor of ACM Transactions on Programming Languages and Systems, ACM Formal Aspects of Computing, Mathematical Structures in Computer Science, Journal of Logical Algebraic Methods in Programming, and the chief editor of The Computer-aided Verification and Concurrency Column for EATCS Bulletin.