pith. sign in

arxiv: 2505.17676 · v3 · submitted 2025-05-23 · 💻 cs.PL

Asynchronous Global Protocols, Precisely: Full Proofs

Kai Pischke , Jake Masters , Nobuko Yoshida This is my paper

Pith reviewed 2026-05-19 14:00 UTC · model grok-4.3

classification 💻 cs.PL
keywords multiparty session typesasynchronous communicationendpoint projectionoperational correspondencetype soundnessdeadlock freedomlivenessglobal protocols
0
0 comments X

The pith

Global protocols can be projected to optimised asynchronous local types while preserving soundness and liveness through a proven operational correspondence.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper develops a top-down methodology for multiparty session types in asynchronous settings. It begins by defining new operational semantics for global protocols that permit sound reorderings of messages. From there it introduces an asynchronous association that links each global protocol to a collection of locally optimised types, then proves that this association is both sound and complete with respect to the operational semantics. Because the association is an invariant, theorems already known for unoptimised bottom-up systems transfer directly to the optimised top-down system, yielding type soundness, session fidelity, deadlock freedom and liveness for the final collection of components.

Core claim

The paper shows that the coinductive full merging projection is correct for the first time, and that the asynchronous association between a global protocol and its optimised local types is both sound and complete. These two results together make the association an invariant that carries type soundness, session-fidelity, deadlock-freedom and liveness from the unoptimised system to any system obtained by independent local optimisations.

What carries the argument

The asynchronous association, a relation that connects a global protocol to a set of refined local types while maintaining operational correspondence under asynchronous message passing.

If this is right

  • Each participant can refine its local type by reordering actions without consulting the others, yet the whole system remains compatible.
  • Type soundness, session fidelity, deadlock freedom and liveness hold for any collection of optimised endpoints that satisfy the asynchronous association.
  • The same invariant can be reused to transfer future bottom-up theorems to the top-down optimised setting without repeating the proofs.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same style of association could be applied to other global description languages that admit asynchronous optimisations.
  • Because local refinements are independent, the approach supports incremental verification of large distributed systems where only some participants change their behaviour.
  • If the operational semantics can be shown to match a concrete network model such as TCP with out-of-order delivery, the liveness guarantees would apply directly to deployed code.

Load-bearing premise

The new operational semantics for global protocols must correctly capture exactly the reorderings that are safe in real asynchronous networks.

What would settle it

A concrete global protocol, its projected local types, and a permitted local optimisation such that the optimised endpoints produce a message sequence forbidden by the original global protocol or that deadlocks while the global protocol does not.

Figures

Figures reproduced from arXiv: 2505.17676 by Jake Masters, Kai Pischke, Nobuko Yoshida.

Figure 1
Figure 1. Figure 1: Top-down methodology of multiparty session types. 𝐺 denotes a global type, which is projected into the three participants, 𝚙, 𝚚 and 𝚛, generating local types 𝑇 𝚙 , 𝑇 𝚚 and 𝑇 𝚛 for each participant. Local types are then refined to 𝑇 opt 𝚙 , 𝑇 opt 𝚚 and 𝑇 opt 𝚛 . Three distributed programs 𝑃𝚙 , 𝑃𝚚 and 𝑃𝚛 follow. In this article, we consider asynchronous communication which is modelled using infinite FIFO que… view at source ↗
Figure 2
Figure 2. Figure 2: Message sequence chart for 𝐺ring (one unfolding of 𝜇𝐭). 𝚙 𝚚 𝚛 𝚙 𝚚 𝚛 𝚙 𝚚 𝚛 𝚙 𝚚 𝚛 𝚙 𝚚 𝚛 𝚙 𝚚 𝚛 𝚙 𝚚 𝚛 𝚙 𝚚 𝚛 (a) projection of 𝐺ring (b) optimised projection of 𝐺ring [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Ring protocol: Projected and optimised interactions (from [16]) 2. 𝚚 sends an integer 𝑚 to 𝚛 labelled by 𝖺𝖽𝖽 or 𝗌𝗎𝖻; (a) if 𝖺𝖽𝖽 is selected, it sends the integer 𝑚 + 𝑘 labelled by 𝖺𝖽𝖽 to 𝚙, and the protocol restarts from Step 1; and (b) if 𝗌𝗎𝖻 is selected, it sends the integer 𝑚 − 𝑘 labelled by 𝗌𝗎𝖻 to 𝚙, and the protocol restarts from Step 1. Global types are semantically similar to more traditional protoc… view at source ↗
Figure 4
Figure 4. Figure 4: Syntax of types. For completing the top-down system with ⩽a , many critical components have been missing, up until now, including (1) the operational correspondence between global types and associated typing contexts (§ 5.2), (2) correctness of coinductive full projection for asynchronous session types (§2.2), and (3) liveness, deadlock-freedom and safety of local types projected from a global protocol (§ … view at source ↗
Figure 5
Figure 5. Figure 5: Global type transition rules. The semantics of global types reflect the behaviours permitted by asynchronous subtyping by allowing specific behaviours to be executed with a type. • [GR-𝜇] permits a valid transition to take place under a recursion binder. • [GR-&] describes the receiving of asynchronous messages, allowing en-route message to be received. • [GR-⊕] describes the sending of asynchronous messag… view at source ↗
Figure 6
Figure 6. Figure 6: Typing context transition rules. 3.2. Semantics of Typing Contexts After introducing the semantics of global types, we now present an LTS semantics for typing contexts, which are collections of local types. The formal definition of a typing context is provided in Def. 8, followed by its transition rules in Def. 9. We then define safety, freedom, and liveness for contexts in Def. 12. Definition 8 (Typing Co… view at source ↗
Figure 7
Figure 7. Figure 7: Local type transition rules. Lemma 7 (Merge has an Operational Correspondence). • If 𝑇𝑖 𝛼 ←←←←→ 𝑇 ′ 𝑖 for all 𝑖 ∈ 𝐼 and ⨅ {𝑇𝑖 ∶ 𝑖 ∈ 𝐼} ∋ 𝑇 , then there exists 𝑇 ′ such that 𝑇 𝛼 ←←←←→ 𝑇 ′ and ⨅ {𝑇 ′ 𝑖 ∶ 𝑖 ∈ 𝐼} ∋ 𝑇 ′ . • If ⨅ {𝑇𝑖 ∶ 𝑖 ∈ 𝐼} ∋ 𝑇 and 𝑇 𝛼 ←←←←→ 𝑇 ′ , then there is some non-empty 𝐽 ⊆ 𝐼 such that 𝑇𝑖 𝛼 ←←←←→ 𝑇 ′ 𝑖 for 𝑖 ∈ 𝐽 and ⨅ {𝑇 ′ 𝑖 ∶ 𝑖 ∈ 𝐽} ∋ 𝑇 ′ . Proof. This is immediate from inverting the to… view at source ↗
Figure 8
Figure 8. Figure 8: Local type context with normal and forgetful holes for 𝑇 opt 𝚚 from the ring protocol. Left: The context where 𝚚 selects a branch to send to 𝚛. The add branch leads to a normal hole [⋅] 1 (tracked continuation), while sub leads to a forgetful hole ⟨⋅⟩2 (to be forgotten). Right: After applying 𝕃, only the add branch remains. forgetful hole indexing set 𝐼 ′ . We require the indexing sets of continuations to … view at source ↗
Figure 9
Figure 9. Figure 9: Bottom-up methodology for multiparty session types. Processes 𝑃𝚙 , 𝑃𝚚 and 𝑃𝚛 are typed by local types 𝑇 𝚙 , 𝑇 𝚚 and 𝑇 𝚛 , which are jointly model-checked against the property 𝜑 [PITH_FULL_IMAGE:figures/full_fig_p033_9.png] view at source ↗
read the original abstract

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 global protocol. We propose a top-down approach, starting with the global protocol which is then projected into a set of local specifications. Next, we use an asynchronous refinement relation, precise asynchronous multiparty subtyping, to enable local specifications to be optimised by permuting actions within individual asynchronous components. This supports local reasoning, as each component can be independently developed and refined in isolation, before being integrated into a larger system. We show that this methodology guarantees both type soundness and liveness of the collection of optimised components. In this article, we first propose new operational semantics of global protocols which capture sound optimisations in the context of asynchronous message-passing. Next we define an asynchronous association between global protocols and a set of optimised local types. Thirdly, we prove, for the first time, the correctness of the most expressive endpoint projection in the literature, coinductive full merging projection. We then show the main theorems of this article: soundness and completeness of the operational correspondence of the asynchronous association. As a consequence, the association acts as an invariant that can be used to transfer key theorems from the bottom-up system to the top-down system. In particular, we used this to prove type soundness, session-fidelity, deadlock-freedom and liveness of the collection of optimised endpoints.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 2 minor

Summary. The manuscript proposes a top-down methodology for asynchronous multiparty session types. It begins with global protocols, introduces new operational semantics to capture sound optimizations under asynchrony, projects them via coinductive full merging projection to optimized local types using precise asynchronous multiparty subtyping, and defines an asynchronous association. The paper proves the correctness of this projection for the first time and establishes soundness and completeness of the operational correspondence, which serves as an invariant to transfer type soundness, session-fidelity, deadlock-freedom, and liveness from the bottom-up system to the optimized top-down endpoints.

Significance. If the central results hold, the work delivers the first full proofs of correctness for the most expressive endpoint projection in the literature (coinductive full merging projection) in an asynchronous setting. The operational correspondence theorems provide a reusable invariant for transferring key safety and liveness properties, supporting independent local optimization of components while preserving global protocol guarantees. This strengthens formal methods for verifying asynchronous distributed systems.

major comments (1)
  1. [§3] §3 (New operational semantics of global protocols): The claim that these semantics capture sound optimizations under asynchronous message-passing is load-bearing for all subsequent results. The presentation does not explicitly demonstrate that the permitted reorderings match exactly those realizable under standard models (per-channel FIFO queues with no implicit cross-channel buffering). A concrete example or lemma showing that a reordering allowed here is realizable in a realistic network (and conversely that unrealizable ones are forbidden) is needed to confirm the correspondence theorems apply to actual implementations.
minor comments (2)
  1. The abstract and introduction could include a brief illustrative example of an optimization permitted by the new semantics and the corresponding local types to aid reader intuition.
  2. Notation for the asynchronous association (e.g., the relation symbol and its coinductive definition) should be introduced with a small running example before the main theorems.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their careful reading and constructive comments on the manuscript. We address the major comment below and will revise the paper to incorporate the requested clarification.

read point-by-point responses

  1. Referee: [§3] §3 (New operational semantics of global protocols): The claim that these semantics capture sound optimizations under asynchronous message-passing is load-bearing for all subsequent results. The presentation does not explicitly demonstrate that the permitted reorderings match exactly those realizable under standard models (per-channel FIFO queues with no implicit cross-channel buffering). A concrete example or lemma showing that a reordering allowed here is realizable in a realistic network (and conversely that unrealizable ones are forbidden) is needed to confirm the correspondence theorems apply to actual implementations.

    Authors: We agree that the presentation in §3 would benefit from an explicit demonstration that the permitted reorderings align precisely with those realizable under standard asynchronous models using per-channel FIFO queues and no cross-channel buffering. The semantics were designed to model exactly such behavior by allowing independent actions across channels while preserving FIFO order within each. In the revised manuscript we will add a new lemma in §3 establishing a correspondence (via simulation or bisimulation) between our reduction rules and executions in a network model consisting of independent FIFO queues per channel. We will also include a concrete example of a permitted reordering (e.g., swapping sends on distinct channels) that is realizable in a realistic asynchronous network, together with an explanation of why reorderings requiring cross-channel buffering or violating per-channel FIFO are forbidden by the rules. This addition will directly support the subsequent correctness results. revision: yes

Circularity Check

0 steps flagged

No circularity: definitions followed by independent formal proofs

full rationale

The paper defines new operational semantics for global protocols under asynchrony, an asynchronous association to optimised local types, and coinductive full merging projection. It then proves correctness of the projection and soundness/completeness of the operational correspondence, using the association as an invariant to transfer properties like type soundness, session-fidelity, deadlock-freedom and liveness. These are standard definitional steps followed by theorem proofs with no reduction of results to inputs by construction, no fitted parameters renamed as predictions, and no load-bearing self-citations that would render the claims tautological. The derivation chain is self-contained against the stated semantics and proofs.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The paper relies on standard coinductive reasoning and operational semantics from process calculi; no free parameters or new postulated entities are mentioned in the abstract.

axioms (2)
  • standard math Coinductive definitions suffice for precise asynchronous multiparty subtyping and full merging projection
    Invoked when defining the refinement relation and the projection operation.
  • domain assumption New operational semantics for global protocols correctly model asynchronous message-passing optimisations
    Introduced as the first technical step and used as the base for all subsequent correspondence proofs.

pith-pipeline@v0.9.0 · 5781 in / 1416 out tokens · 107431 ms · 2026-05-19T14:00:49.502659+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

57 extracted references · 57 canonical work pages

  1. [1]

    Recommendation Z.120, International Telecommunication Union (ITU-T), Geneva, October 1996

    Message sequence chart (msc). Recommendation Z.120, International Telecommunication Union (ITU-T), Geneva, October 1996. (10/96). Revised and approved by WTSC (Geneva, 9–18 Oct 1996)

    work page 1996

  2. [2]

    Generalised Multiparty Session Types with Crash-Stop Failures (Technical Report, 2022-07-08)

    Adam D Barwell, Alceste Scalas, Nobuko Yoshida, and Fangyi Zhou. Generalised Multiparty Session Types with Crash-Stop Failures (Technical Report, 2022-07-08)

    work page 2022

  3. [3]

    Asynchronous subtyping by trace relaxation

    Laura Bocchi, Andy King, and Maurizio Murgia. Asynchronous subtyping by trace relaxation. In Bernd FinkbeinerandLauraKovács, editors,ToolsandAlgorithmsfortheConstruction andAnalysisofSystems-30th InternationalConference,TACAS2024,HeldasPartoftheEuropeanJointConferencesonTheoryandPractice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 20...

    work page 2024

  4. [4]

    Abstract Subtyping for Asynchronous Multiparty Sessions

    Laura Bocchi, Andy King, Maurizio Murgia, and Simon Thompson. Abstract Subtyping for Asynchronous Multiparty Sessions. In Patricia Bouyer and Jaco van de Pol, editors,36th International Conference on ConcurrencyTheory(CONCUR2025),volume348ofLeibnizInternationalProceedingsinInformatics(LIPIcs), pages 10:1–10:19, Dagstuhl, Germany, 2025. Schloss Dagstuhl – ...

    work page 2025

  5. [5]

    On Communicating Finite-State Machines.Journal of the ACM, 30(2):323– 342, April 1983

    Daniel Brand and Pitro Zafiropulo. On Communicating Finite-State Machines.Journal of the ACM, 30(2):323– 342, April 1983

    work page 1983

  6. [6]

    A Sound Algorithm for Asynchronous Session Subtyping and its Implementation.Logical Methods in Computer Science, Volume 17, Issue 1, March 2021

    Mario Bravetti, Marco Carbone, Julien Lange, Nobuko Yoshida, and Gianluigi Zavattaro. A Sound Algorithm for Asynchronous Session Subtyping and its Implementation.Logical Methods in Computer Science, Volume 17, Issue 1, March 2021

    work page 2021

  7. [7]

    Undecidabilityofasynchronoussessionsubtyping.Inf

    MarioBravetti,MarcoCarbone,andGianluigiZavattaro. Undecidabilityofasynchronoussessionsubtyping.Inf. Comput., 256:300–320, 2017

    work page 2017

  8. [8]

    A Sound and Complete Characterization of Fair AsynchronousSessionSubtyping

    Mario Bravetti, Luca Padovani, and Gianluigi Zavattaro. A Sound and Complete Characterization of Fair AsynchronousSessionSubtyping. InPatriciaBouyerandJacovandePol,editors,36thInternationalConference on Concurrency Theory (CONCUR 2025), volume 348 ofLeibniz International Proceedings in Informatics (LIPIcs), pages 11:1–11:17, Dagstuhl, Germany, 2025. Schlo...

    work page 2025

  9. [9]

    Structuredcommunication-centeredprogrammingforweb services.ACM Trans

    MarcoCarbone,KoheiHonda,andNobukoYoshida. Structuredcommunication-centeredprogrammingforweb services.ACM Trans. Program. Lang. Syst., 34(2):8:1–8:78, 2012

    work page 2012

  10. [10]

    Zooid: a DSL for certified multiparty computation: from mechanised metatheory to certified multiparty processes

    David Castro-Perez, Francisco Ferreira, Lorenzo Gheri, and Nobuko Yoshida. Zooid: a DSL for certified multiparty computation: from mechanised metatheory to certified multiparty processes. In Stephen N. Freund and Eran Yahav, editors,PLDI ’21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Virtual Event, Canada...

    work page 2021

  11. [11]

    CAMP:cost-awaremultipartysessionprotocols.Proc.ACMProgram

    DavidCastro-PerezandNobukoYoshida. CAMP:cost-awaremultipartysessionprotocols.Proc.ACMProgram. Lang., 4(OOPSLA):155:1–155:30, 2020

    work page 2020

  12. [12]

    On the preciseness of subtyping in session types.Logical Methods in Computer Science, 13(2), June 2017

    Tzu Chun Chen, Mariangiola Dezani-Ciancaglini, Alceste Scalas, and Nobuko Yoshida. On the preciseness of subtyping in session types.Logical Methods in Computer Science, 13(2), June 2017

    work page 2017

  13. [13]

    On the preciseness of subtyping in session types: 10 years later

    Tzu-Chun Chen, Mariangiola Dezani-Ciancaglini, and Nobuko Yoshida. On the preciseness of subtyping in session types: 10 years later. InProceedings of the 26th International Symposium on Principles and Practice of Declarative Programming, PPDP ’24, New York, NY, USA, 2024. Association for Computing Machinery. K. Pischke et al.:Preprint submitted to Elsevie...

    work page 2024

  14. [14]

    A Gentle Introduction to Multiparty Asynchronous Session Types

    Mario Coppo, Mariangiola Dezani-Ciancaglini, Luca Padovani, and Nobuko Yoshida. A Gentle Introduction to Multiparty Asynchronous Session Types. In15th International School on Formal Methods for the Design of Computer, Communication and Software Systems: Multicore Programming, volume 9104 ofLNCS, pages 146–178. Springer, 2015

    work page 2015

  15. [15]

    Global Progress for Dynamically Interleaved Multiparty Sessions.MSCS, 26:238–302, 2015

    Mario Coppo, Mariangiola Dezani-Ciancaglini, Nobuko Yoshida, and Luca Padovani. Global Progress for Dynamically Interleaved Multiparty Sessions.MSCS, 26:238–302, 2015

    work page 2015

  16. [16]

    Safesession-basedasynchronouscoordinationinrust

    ZakCutnerandNobukoYoshida. Safesession-basedasynchronouscoordinationinrust. InCoordinationModels and Languages: 23rd IFIP WG 6.1 International Conference, COORDINATION 2021, Held as Part of the 16th InternationalFederatedConferenceonDistributedComputingTechniques,DisCoTec2021,Valletta,Malta,June 14–18, 2021, Proceedings, page 80–89, Berlin, Heidelberg, 20...

    work page 2021

  17. [17]

    Deadlock-Free Asynchronous Message Reordering in Rust with Multiparty Session Types

    Zak Cutner, Nobuko Yoshida, and Martin Vassor. Deadlock-Free Asynchronous Message Reordering in Rust with Multiparty Session Types. In27th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, volume abs/2112.12693 ofPPoPP ’22, pages 246–261. ACM, 2022

    work page arXiv 2022

  18. [18]

    Full abstraction in a subtyped pi-calculus with linear types

    Romain Demangeon and Kohei Honda. Full abstraction in a subtyped pi-calculus with linear types. In Proceedings of CONCUR 2011, volume 6901 ofLNCS, pages 280–296. Springer, 2011

    work page 2011

  19. [19]

    Multiparty session types meet communicating automata

    Pierre-Malo Deniélou and Nobuko Yoshida. Multiparty session types meet communicating automata. InESOP, volume 7211 ofLNCS, pages 194–213. Springer, 2012

    work page 2012

  20. [20]

    Multiparty compatibility in communicating automata: Characteri- sation and synthesis of global session types

    Pierre-Malo Deniélou and Nobuko Yoshida. Multiparty compatibility in communicating automata: Characteri- sation and synthesis of global session types. InICALP 2013, pages 174–186, 2013

    work page 2013

  21. [21]

    Parameterisedmultipartysessiontypes

    Pierre-MaloDeniélou,NobukoYoshida,AndiBejleri,andRaymondHu. Parameterisedmultipartysessiontypes. Logical Methods in Computer Science, 8(4), 2012

    work page 2012

  22. [22]

    Realisability and complementability of multiparty session types

    Cinzia Di Giusto, Etienne Lozes, and Pascal Urso. Realisability and complementability of multiparty session types. InProceedings of the 27th International Symposium on Principles and Practice of Declarative Programming, PPDP ’25, New York, NY, USA, 2025. Association for Computing Machinery

    work page 2025

  23. [23]

    Burak Ekici, Tadayoshi Kamegai, and Nobuko Yoshida. Formalising Subject Reduction and Progress for MultipartySessionProcesses.In16thInternationalConferenceonInteractiveTheoremProving,2025,Reykjavik, Iceland, volume 352 ofLIPIcs, pages 19:1–19:23. Schloss Dagstuhl - Leibniz-Zentrum f"ur Informatik, 2025

    work page 2025

  24. [24]

    Completeness of Asynchronous Session Tree Subtyping in Coq

    Burak Ekici and Nobuko Yoshida. Completeness of Asynchronous Session Tree Subtyping in Coq. In15th International Conference on Interactive Theorem Proving, 2024, Tbilisi, Georgia, volume 309, pages 6:1–6:20. Schloss Dagstuhl - Leibniz-Zentrum f"ur Informatik, 2024

    work page 2024

  25. [25]

    SimonGayandMalcolmHole.Subtypingforsessiontypesinthepicalculus.ActaInformatica,42(2-3):191–225, November 2005

    work page 2005

  26. [26]

    Precise subtyping for synchronous multiparty sessions.Journal of Logical and Algebraic Methods in Programming, 104:127–173, April 2019

    Silvia Ghilezan, Svetlana Jakšić, Jovanka Pantović, Alceste Scalas, and Nobuko Yoshida. Precise subtyping for synchronous multiparty sessions.Journal of Logical and Algebraic Methods in Programming, 104:127–173, April 2019

    work page 2019

  27. [27]

    Precise subtyping for asynchronous multiparty sessions.ACM Trans

    Silvia Ghilezan, Jovanka Pantović, Ivan Prokić, Alceste Scalas, and Nobuko Yoshida. Precise subtyping for asynchronous multiparty sessions.ACM Trans. Comput. Logic, 24(2), nov 2023

    work page 2023

  28. [28]

    The standardization of message sequence charts

    Peter Graubmann, Ekkart Rudolph, and Jens Grabowski. The standardization of message sequence charts. In ProceedingsoftheIEEESoftwareEngineeringStandardsSymposium(SESS’93),pages48–63,Brighton,United Kingdom, September 1993. IEEE Computer Society

    work page 1993

  29. [29]

    JonasKastbergHinrichsen,JesperBengtson,andRobbertKrebbers.Actris2.0:Asynchronoussession-typebased reasoning in separation logic.Logical Methods in Computer Science, Volume 18, Issue 2, Jun 2022. K. Pischke et al.:Preprint submitted to ElsevierPage 40 of 47 Asynchronous Global Protocols, Precisely

    work page 2022

  30. [30]

    Languageprimitivesandtypedisciplinesforstructured communication-based programming

    KoheiHonda,VascoT.Vasconcelos,andMakotoKubo. Languageprimitivesandtypedisciplinesforstructured communication-based programming. InProceedings of ESOP 1998, volume 1381 ofLNCS, pages 22–138. Springer, 1998

    work page 1998

  31. [31]

    Type-Directed Compilation for Multicore Programming.ENTCS, 241:101–111, 2009

    Kohei Honda, Vasco Thudichum Vasconcelos, and Nobuko Yoshida. Type-Directed Compilation for Multicore Programming.ENTCS, 241:101–111, 2009

    work page 2009

  32. [32]

    Multiparty Asynchronous Session Types

    Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty Asynchronous Session Types. InProceedings of POPL 2008, pages 273–284. ACM, 2008

    work page 2008

  33. [33]

    Multiparty asynchronous session types.Journal of the ACM, 63(1):9:1–9:67, 2016

    Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types.Journal of the ACM, 63(1):9:1–9:67, 2016

    work page 2016

  34. [34]

    On the Undecidability of Asynchronous Session Subtyping

    Julien Lange and Nobuko Yoshida. On the Undecidability of Asynchronous Session Subtyping. InProceedings of FOSSACS 2017, volume 10203 ofLNCS, pages 441–457. Springer, 2017

    work page 2017

  35. [35]

    Deciding subtyping for asynchronous multiparty sessions

    Elaine Li, Felix Stutz, and Thomas Wies. Deciding subtyping for asynchronous multiparty sessions. InLecture Notes in Computer Science, Lecture notes in computer science, pages 176–205. Springer Nature Switzerland, Cham, 2024

    work page 2024

  36. [36]

    Complete multiparty session type projection with automata

    Elaine Li, Felix Stutz, Thomas Wies, and Damien Zufferey. Complete multiparty session type projection with automata. InLecture Notes in Computer Science, Lecture notes in computer science, pages 350–373. Springer Nature Switzerland, Cham, 2023

    work page 2023

  37. [37]

    Characterizingimplementabilityofglobalprotocols with infinite states and data.Proc

    ElaineLi,FelixStutz,ThomasWies,andDamienZufferey. Characterizingimplementabilityofglobalprotocols with infinite states and data.Proc. ACM Program. Lang., 9(OOPSLA1), April 2025

    work page 2025

  38. [38]

    Certified Implementability of Global Multiparty Protocols

    Elaine Li and Thomas Wies. Certified Implementability of Global Multiparty Protocols. In Yannick Forster and Chantal Keller, editors,16th International Conference on Interactive Theorem Proving (ITP 2025), volume 352 ofLeibniz International Proceedings in Informatics (LIPIcs), pages 15:1–15:20, Dagstuhl, Germany, 2025. Schloss Dagstuhl – Leibniz-Zentrum f...

    work page 2025

  39. [39]

    On subtyping-relation completeness, with an application to iso-recursive types.ACM Trans

    Jay Ligatti, Jeremy Blackburn, and Michael Nachtigal. On subtyping-relation completeness, with an application to iso-recursive types.ACM Trans. Program. Lang. Syst., 39(1), March 2017

    work page 2017

  40. [40]

    A behavioral notion of subtyping.ACM Trans

    Barbara H Liskov and Jeannette M Wing. A behavioral notion of subtyping.ACM Trans. Program. Lang. Syst., 16(6):1811–1841, November 1994

    work page 1994

  41. [41]

    Generalising projection in asyn- chronousmultipartysessiontypes

    Rupak Majumdar, Madhavan Mukund, Felix Stutz, and Damien Zufferey. Generalising projection in asyn- chronousmultipartysessiontypes. InSergeHaddadandDanieleVaracca,editors,32ndInternationalConference on Concurrency Theory, CONCUR 2021, August 24-27, 2021, Virtual Conference, volume 203 ofLIPIcs, pages 35:1–35:24. Schloss Dagstuhl - Leibniz-Zentrum für Info...

    work page 2021

  42. [42]

    Session-based communication optimisation for higher-order mobile processes

    Dimitris Mostrous and Nobuko Yoshida. Session-based communication optimisation for higher-order mobile processes. InPierre-LouisCurien,editor,TypedLambdaCalculiandApplications,9thInternationalConference, TLCA 2009, Brasilia, Brazil, July 1-3, 2009. Proceedings, volume 5608 ofLecture Notes in Computer Science, pages 203–218. Springer, 2009

    work page 2009

  43. [43]

    Coutinho, and Nobuko Yoshida

    Nicholas Ng, Jose G.F. Coutinho, and Nobuko Yoshida. Protocols by Default: Safe MPI Code Generation based on Session Types. In24th International Conference on Compiler Construction, volume 9031 ofLNCS, pages 212–232. Springer, 2015

    work page 2015

  44. [44]

    Multiparty Session C: Safe Parallel Programming with Message Optimisation

    Nicholas Ng, Nobuko Yoshida, and Kohei Honda. Multiparty Session C: Safe Parallel Programming with Message Optimisation. In50th International Conference on Objects, Models, Components, Patterns, volume 7304 ofLNCS, pages 202–218. Springer, 2012

    work page 2012

  45. [45]

    MIT Press, 2002

    Benjamin Pierce.Types and Programming Languages. MIT Press, 2002. K. Pischke et al.:Preprint submitted to ElsevierPage 41 of 47 Asynchronous Global Protocols, Precisely

    work page 2002

  46. [46]

    Asynchronous Global Protocols, Precisely

    Kai Pischke and Nobuko Yoshida. Asynchronous Global Protocols, Precisely. InComponents Operationally: Reversibility and System Engineering, volume 16065 ofLNCS, pages 116–133. Springer Nature, 2025

    work page 2025

  47. [47]

    Less is more: Multiparty session types revisited.Proceedings of the ACM on Programming Languages, 3(POPL):1–29, January 2019

    Alceste Scalas and Nobuko Yoshida. Less is more: Multiparty session types revisited.Proceedings of the ACM on Programming Languages, 3(POPL):1–29, January 2019

    work page 2019

  48. [48]

    Asynchronous Multiparty Session Type Implementability is Decidable - Lessons Learned from Message Sequence Charts

    Felix Stutz. Asynchronous Multiparty Session Type Implementability is Decidable - Lessons Learned from Message Sequence Charts. In Karim Ali and Guido Salvaneschi, editors,37th European Conference on Object-OrientedProgramming(ECOOP2023),volume263ofLeibnizInternationalProceedingsinInformatics (LIPIcs), pages 32:1–32:31, Dagstuhl, Germany, 2023. Schloss Da...

    work page 2023

  49. [49]

    An automata-theoretic basis for specification and type checking of multiparty protocols

    Felix Stutz and Emanuele D’Osualdo. An automata-theoretic basis for specification and type checking of multiparty protocols. InProgramming Languages and Systems: 34th European Symposium on Programming, ESOP 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Hamilton, ON, Canada, May 3–8, 2025, Proceed...

    work page 2025

  50. [50]

    An Interaction-based Language and its Typing System

    Kaku Takeuchi, Kohei Honda, and Makoto Kubo. An Interaction-based Language and its Typing System. In Constantine Halatsis, Dimitris G. Maritsas, George Philokyprou, and Sergios Theodoridis, editors,PARLE ’94: Parallel Architectures and Languages Europe, 6th International PARLE Conference, Athens, Greece, July 4-8, 1994, Proceedings, volume 817 ofLecture N...

    work page 1994

  51. [51]

    Top-down or bottom-up? complexity analyses of synchronous multiparty session types.Proc

    Thien Udomsrirungruang and Nobuko Yoshida. Top-down or bottom-up? complexity analyses of synchronous multiparty session types.Proc. ACM Program. Lang., 9(POPL):1040–1071, 2025

    work page 2025

  52. [52]

    Adecentralizedanalysisofmultipartyprotocols.Sci.Comput.Program., 222(102840):102840, October 2022

    BasvandenHeuvelandJorgeAPérez. Adecentralizedanalysisofmultipartyprotocols.Sci.Comput.Program., 222(102840):102840, October 2022

    work page 2022

  53. [53]

    Programming language implementations with multiparty session types

    Nobuko Yoshida. Programming language implementations with multiparty session types. In Frank S. deBoer,FerruccioDamiani,ReinerHähnle,EinarBrochJohnsen,andEduardKamburjan,editors,ActiveObject Languages: Current Research Trends, volume 14360 ofLecture Notes in Computer Science, pages 147–165. Springer, 2024

    work page 2024

  54. [54]

    Less is More Revisited: Association with Global Multiparty Session Types

    Nobuko Yoshida and Ping Hou. Less is More Revisited: Association with Global Multiparty Session Types. In The Practice of Formal Methods: Essays in Honour of Cliff Jones, Part II, pages –. LNCS, 2024

    work page 2024

  55. [55]

    The Scribble Protocol Language

    Nobuko Yoshida, Raymond Hu, Rumyana Neykova, and Nicholas Ng. The Scribble Protocol Language. In 8th International Symposium on Trustworthy Global Computing, volume 8358 ofLNCS, pages 22–41. Springer, 2013

    work page 2013

  56. [56]

    Session-based compilation framework for multicore programming

    Nobuko Yoshida, Vasco Thudichum Vasconcelos, Hervé Paulino, and Kohei Honda. Session-based compilation framework for multicore programming. InFMCO 2008, pages 226–246, 2008

    work page 2008

  57. [57]

    CommunicatingFiniteStateMachinesandanExtensible Toolchain for Multiparty Session Types

    NobukoYoshida,FangyiZhou,andFranciscoFerreira. CommunicatingFiniteStateMachinesandanExtensible Toolchain for Multiparty Session Types. In23rd International Symposium on Fundamentals of Computation Theory, volume 12867 ofLNCS, pages 18–35. Springer, 2021. K. Pischke et al.:Preprint submitted to ElsevierPage 42 of 47 Asynchronous Global Protocols, Precisely...

    work page 2021