7 papers
Mixed Choice Multiparty Session Types, Precisely
Jake Masters, Nobuko Yoshida
A precise (sound and complete) subtyping relation specifies that is a subtype of if and only if a program of type can always safely replace a program of type $…
Top-down = Bottom-up: Sound and Complete Characterisations of Liveness by Multiparty Global Protocols
Kai Pischke, Nobuko Yoshida
Multiparty session types (MPST) are a type discipline for concurrent and distributed systems, designed to ensure not only type safety and deadlock-freedom, but also liveness of typ…
Formally Verified Liveness with Multiparty Session Types in Rocq
Omer Keskin, Nobuko Yoshida, Rob van Glabbeek
Multiparty session types (MPST) offer a framework for the description of communication-based protocols involving multiple participants. In the top-down approach to MPST, the commun…
Asynchronous Global Protocols, Precisely: Full Proofs
Kai Pischke, Jake Masters, Nobuko Yoshida
Asynchronous multiparty session types are a type-based framework which ensure the compatibility of components in a distributed system by checking compliance against a specified glo…
Denotational reasoning for asynchronous multiparty session types
Dylan McDermott, Nobuko Yoshida
We provide the first denotational semantics for asynchronous multiparty session types with precise asynchronous subtyping. Our semantics enables us to reason about asynchronous mes…
On Asynchronous Multiparty Session Types for Federated Learning
Ivan ProkiÄ, Simona ProkiÄ, Silvia Ghilezan +2
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 asy…