Multiparty and Asynchronous Session Types

Prerequisites. Direct starred prerequisites: Chapter 21. No later core chapter depends on this route.

Three pairwise-dual channels need not compose into one coherent conversation. For three channels directed $B\to A$, $C\to B$, and $A\to C$, consider Every channel has one sender and one receiver with the same payload type, yet the parallel composition has three leading inputs and no step. Multiparty session types begin from a global protocol and project one local view per participant. Asynchronous execution adds queues, so the proof must also relate messages already sent to actions not yet received.

This chapter uses Honda, Yoshida, and Carbone for the historical global/local architecture and its motivating obstruction [HYC16]. It does not use their flawed projection argument as the owner of subject reduction. That theorem belongs to the repaired, mechanized calculus of Tirore, Bengtson, and Carbone [TBC25].

The repaired asynchronous calculus

Let $p,q,r$ range over roles, $k$ over explicit queue addresses, and $s^p$ over a session located at role $p$. The load-bearing process forms are A tilde denotes a finite sequence: $\tilde{s}$ is the located session family bound with $s$, and $\tilde{h}$ is one queue’s item sequence. A queue item is a value, delegated endpoint, or label annotated by its sender. A send appends to $s[k]$; the matching receive consumes only the head item whose sender is the expected role. Session initiation creates the finite family of queues declared by the requester. Definitions, conditionals, and structural congruence complete the process dynamics.

Closed, contractive global and local types are The paper’s restriction on recursion rejects every subexpression $$\mu t_0.\mu t_1\dots \mu t_n.t_0.$$ This prevents projection from manufacturing an unguarded local loop.

The global and local labelled semantics are asynchronous. A later interaction may move beneath an earlier one when it does not involve the blocked receiver; a local action may move beneath an output on a different queue address. With these rules, full projection both simulates and reflects global transitions. The pinned Coq development names the directions harmony_sound and harmony_complete.

The three global clauses are independent. Without projectability, a role absent from a choice can be asked to guess its continuation. Without linearity, two senders can race to put differently typed values at the same address. For the paper’s counterexample $$p\to q:k_1\{{\ell }_1:q\to r:k_2⟨\mathsf{Bool}⟩.\mathsf{end},{\ell }_2:p\to r:k_2⟨\mathsf{Bool}⟩.\mathsf{end}\},$$ the relaxed barb sees the second branch’s $p$-to-$r$ action, but the true global semantics cannot move that action because its rule requires the same labelled move in every branch. This is a failure of unstuckness, not a wrong-queue-head definition. Sender and label agreement at concrete queue heads instead follows from queue typing and the coherent decomposition. In the mechanization the ingredients are represented by projectable, LinearCo, and goodG; the process typing judgment is OFT.

Write $\mathrm{\Gamma }{⊢}_{D}P{▹}_C\mathrm{\Delta };Q$ for the paper’s typing judgment: shared assumptions $\mathrm{\Gamma }$, definitions $D$, process $P$, session/channel environment $\mathrm{\Delta }$, and queue specification $Q$, under the explicit channel inventory $C$. The rules type each process prefix against the corresponding local action and type each concrete queue against $Q$. Parallel composition splits linear session obligations; restriction checks a whole coherent session rather than hiding unrelated endpoints.

For example, the value-output rule and the matching queue rule have the following local shape; the omitted shared premises are unchanged. $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢e:U\\ \mathrm{\Gamma }{⊢}_{D}P{▹}_C\mathrm{\Delta },s^p:T;Q\end{array}}{\mathrm{\Gamma }{⊢}_D{s}^p[k]!⟨e⟩;P{▹}_C\mathrm{\Delta },s^p:!k⟨U⟩.T;Q}\mathrm{T}-\mathrm{Send}$$ $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢v:U\\ \mathrm{\Gamma }{⊢}_{D}s[k]::\tilde{h}{▹}_C\mathrm{\Delta };Q\end{array}}{\mathrm{\Gamma }{⊢}_{D}s[k]::(\tilde{h}\cdot p!v){▹}_C\mathrm{\Delta };Q\cdot (k,p,U)}\mathrm{T}-\mathrm{Queue}.$$ A send step uses T-Send on the process before the step and T-Queue on the appended sender-tagged item afterward. The session environment advances from $!k⟨U⟩.T$ to $T$, which is the send case used in the preservation proof.

Proof of Theorem 59.4 — Repaired subject reduction

Proof. Induct on the process reduction. Send, delegation, and selection transfer a typed item to the corresponding queue; receive, session receive, and branch use queue typing and environment decomposition to identify the head item and advance its local action. Initiation uses full projection and the projection theorem to create the local family and empty queues. Conditional and definition steps use expression preservation and substitution. Contextual steps rebuild restriction or parallel typing; structural congruence uses its separate invariance theorem. For a communication that completes a global interaction, projection harmony and the coherent global witness—including its coinductive unstuckness premise—produce ${\mathrm{\Delta }}_0\stackrel{\ell }{\to }{\mathrm{\Delta }}_1$; administrative and one-sided queue steps leave ${\mathrm{\Delta }}_0$ unchanged. Linearity gives the dependency fact needed when two actions mention the same explicit queue address. ◻

This theorem is subject_reduction_final in the pinned Coq source; its empty-context specialization is subject_reduction_empty, and structural invariance is OFT_cong. The printed theorem, proof dependencies, and identifiers all belong to the ECOOP 2025 calculus.

Proof of Corollary 59.5 — Communication safety

Proof. The paper first proves syntactic exclusion of error structures, then applies Theorem 59.4 after each step. The corresponding Coq identifiers are $$\mathtt{\text{Error\_struct}},\mathtt{\text{OFT\_not\_error\_struct}},\mathtt{\text{OFT\_not\_error\_sem}}.$$ ◻

Communication safety excludes a wrong value type, sender, or label at a receive. It does not establish progress, general deadlock freedom, freedom from orphan messages, fair delivery, multiparty compatibility, termination, or liveness. A coherent typing premise can also be destroyed by manually assembling endpoints or queues not obtained from one admitted global type.

A complete three-party execution

Use four distinct addresses $k_1,k_2,k_3,k_4$ for Its projections are Abbreviate successive residuals by $B_0,B_1,B_2$, $S_0,\dots ,S_4$, and $K_0,K_1,K_2$, with $B_0=T_B$, $S_0=T_S$, $K_0=T_K$, and each successor obtained by deleting the displayed outer action. In queue order $(k_1,k_2,k_4,k_3)$, the accepting execution is the following fully annotated trace: Each row names the transition and advances exactly one residual type. A send appends a sender-tagged item; a receive checks and removes the head. The refusal branch has the same shape with $\mathsf{no}$ at $k_4$. Every address is used by exactly one global action, so the same-address premise in definition 59.2 never arises and linearity holds vacuously. At the outer branch, both continuations project at $B$ to the same . Equation (Plain-Branch) therefore proves projectability without importing a full-merge operator. The protocol deliberately does not tell $B$ which bank branch was taken.

From protocols to choreographic programs

Pirouette changes the object of study from an asynchronous global protocol to a typed, executable choreography [HG21]. Its local language is a parameter, not silently assumed to be the lambda calculus. The interface requires decidable equality of locations; expressions with capture-avoiding substitution and its equations; a closed class of values that do not step; unique typing with variables, Booleans, exchange, weakening, strengthening, and substitution; and, for relative soundness, Boolean inversion, local preservation, and local progress.

For three distinct locations $A,B,C$, set The higher-order call has the complete principal calculation $$\mathsf{appglobal}(F,V)\stackrel{Global-App}{⟶}A⟨\mathsf{item}⟩\to B;B⟨\mathsf{done}⟩\to C;{\mathsf{ret}}_C(0).$$ The step substitutes $V$ for $X$; the leading synchronization prevents one endpoint from entering the substituted choreography before the others have finished evaluating the global function and argument.

A choreography’s small-step semantics carries a block set: a location whose pending action is blocked cannot be used by an out-of-order step, while independent locations may compute or communicate past it. Communication is synchronous. A higher-order call performs a global synchronization before entering its body; that barrier is operational, not merely an EPP artifact.

The branch-knowledge obstruction is already visible in Projection gives $B$ an offer from $A$ before its branch-specific send. A hand-written endpoint that sends $1$ immediately omits that offer. If the two selections are deleted from the choreography, projection at $B$ must merge a send of $1$ with a send of $0$, and the partial merge is undefined. This is the deliberately faulty endpoint collection used by the executable comparison.

Proof of Theorem 59.7 — Pirouette relative type soundness

Proof. For preservation, induct on the choreography step. Local computation uses local preservation; communication uses the local substitution law and the typing substitution lemma; selection preserves the chosen continuation; an out-of-order step rebuilds the surrounding construct because its block-set side condition keeps the active locations independent. For progress, inspect the leading construct. Local progress advances a nonvalue expression, Boolean inversion chooses a conditional branch, and closedness rules out a free procedure variable. The communication and selection forms synchronize when their local data are values. ◻

The source proves the preservation and progress clauses separately before combining them into relative type soundness [HG21].

Endpoint projection maps a choreography to one control program per nonempty finite set $L$ of locations. A participant not deciding a branch projects the alternatives with a partial merge; merge retains their common behavior and combines compatible offers. Incompatible hand-written endpoints such as two observers expecting different unannounced branches have no common merge and are rejected. Write $[[C{]]}_L\downarrow$ when every required endpoint merge is defined, $[[C{]]}_L\uparrow$ for undefinedness, and ${\le }_{\mathsf{nd}}$ for the report’s preorder that permits extra local nondeterminism. For a choreography $C$, write $\mathsf{FCV}(C)$ for its free choreography variables and ${\mathsf{FLV}}_p(C)$ for the free local expression variables at location $p$, with the binders in definition 59.6 removing the variables they bind. Define $$\mathsf{PirExprClosed}(C)⟺\mathsf{FCV}(C)=\varnothing \wedge \mathrm{\forall }p.{\mathsf{FLV}}_p(C)=\varnothing .$$ In the choreography typing judgment $\mathrm{\Gamma };\mathrm{\Delta }⊢C:\tau$, $\mathrm{\Gamma }$ assigns types to local expression variables at each location and $\mathrm{\Delta }$ assigns types to choreography variables. Thus $\cdot ;\cdot ⊢C:\tau$ is the closed instance of that judgment; the separate predicate above records syntactic closedness, which endpoint projection preserves across reduction.

Proof of Theorem 59.8 — Pirouette projection card

Imported proof. The technical report proves local completeness and global completeness by induction on the choreography step, and proves soundness by induction on the projected-system step. Its deadlock-freedom argument combines that soundness simulation with choreography progress and preservation. The third clause retains all three boundary premises of the last Coq theorem: the location list is nonempty, every location in $C$ occurs in that list, and $\mathsf{PirExprClosed}(C)$ holds. The result is deadlock freedom for systems reached from well-typed projection. It is not asynchronous queue liveness, arbitrary endpoint equivalence, failure recovery, or correctness of a network runtime. The exact theorem signatures and their substantial inductive proof development are imported from Hirsch and Garg’s endpoint projection metatheory [HG21]. ◻

Chapter seminar

The Kappa corpus at artifacts/ch59-mpst-choreography/ represents the sale protocol as a finite global AST, projects all three roles, and replays its sender-tagged FIFO transitions. A separate choreography AST projects control programs, regenerates them after a source change, and rejects missing branch knowledge. These are executable finite models of the two worked examples, not mechanizations of either theorem card or executions of the pinned Coq developments.