Binary Session Types and Typed Protocols

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

A function type describes one call. A protocol type describes the whole conversation that follows from one channel endpoint. The distinction first appears when a client sends an argument, receives a result, and then reaches the terminal protocol: neither the argument type nor the result type records that order. This chapter fixes a finite, binary, intuitionistic linear session calculus whose proof theory does record it. A later, explicitly marked route studies graded non-linear communication in a different calculus. Results do not transfer between the two cards.

A finite logical session calculus

Session types are propositions of intuitionistic linear logic: The provider of $z:A$ offers the behavior $A$ on $z$. The synchronous binary-choice pi-calculus has grammar A linear context $\mathrm{\Delta }$ contains endpoints that it must use exactly once; an unrestricted context $\mathrm{\Gamma }$ contains replicated services. The judgment is $$\mathrm{\Gamma };\mathrm{\Delta }⊢P::z:A.$$ Names in $\mathrm{\Gamma }$, $\mathrm{\Delta }$, and $z$ are pairwise disjoint. In the rules, $(\nu x)(P\mid Q)$ abbreviates $(\nu x)(P\mid Q)$, and $(\nu y)x⟨y⟩.(P\mid Q)$ abbreviates $(\nu y)x⟨y⟩.(P\mid Q)$. Thus $P$ provides the fresh channel $y$, while $Q$ continues on $x$. These are typed abbreviations, not new process constructors.

The rules below fix the polarity of every constructor. Exchange is admissible for both contexts; contraction and weakening are admissible only for $\mathrm{\Gamma }$.

$\mathrm{\Gamma };\cdot ⊢\mathbf{0}::z:\mathbf{1}$

$\mathrm{\Gamma };\mathrm{\Delta }⊢P::z:C$

$\mathrm{\Gamma };\mathrm{\Delta },x:\mathbf{1}⊢P::z:C$

$\mathrm{\Gamma };{\mathrm{\Delta }}_1⊢P::y:A$$\mathrm{\Gamma };{\mathrm{\Delta }}_2⊢Q::x:B$

$\mathrm{\Gamma };{\mathrm{\Delta }}_1,{\mathrm{\Delta }}_2⊢(\nu y)x⟨y⟩.(P\mid Q)::x:A\otimes B$

$\mathrm{\Gamma };\mathrm{\Delta },y:A,x:B⊢P::z:C$

$\mathrm{\Gamma };\mathrm{\Delta },x:A\otimes B⊢x(y).P::z:C$

$\mathrm{\Gamma };\mathrm{\Delta },y:A⊢P::x:B$

$\mathrm{\Gamma };\mathrm{\Delta }⊢x(y).P::x:A⊸B$

$\mathrm{\Gamma };{\mathrm{\Delta }}_1⊢P::y:A$$\mathrm{\Gamma };{\mathrm{\Delta }}_2,x:B⊢Q::z:C$

$\mathrm{\Gamma };{\mathrm{\Delta }}_1,{\mathrm{\Delta }}_2,x:A⊸B⊢(\nu y)x⟨y⟩.(P\mid Q)::z:C$

$\mathrm{\Gamma };{\mathrm{\Delta }}_1⊢P::x:A$$\mathrm{\Gamma };{\mathrm{\Delta }}_2,x:A⊢Q::z:C$

$\mathrm{\Gamma };{\mathrm{\Delta }}_1,{\mathrm{\Delta }}_2⊢(\nu x)(P\mid Q)::z:C$

For $A\oplus B$, the provider selects and the client branches; for , the client selects and the provider branches. The full additive rule sheet is

$\mathrm{\Gamma };\mathrm{\Delta }⊢P::x:A$

$\mathrm{\Gamma };\mathrm{\Delta }⊢x.\mathsf{inl};P::x:A\oplus B$

$\mathrm{\Gamma };\mathrm{\Delta }⊢P::x:B$

$\mathrm{\Gamma };\mathrm{\Delta }⊢x.\mathsf{inr};P::x:A\oplus B$

$\mathrm{\Gamma };\mathrm{\Delta },x:A⊢P::z:C$$\mathrm{\Gamma };\mathrm{\Delta },x:B⊢Q::z:C$

$\mathrm{\Gamma };\mathrm{\Delta },x:A\oplus B⊢x.\mathsf{case}(P,Q)::z:C$

$\mathrm{\Gamma };\mathrm{\Delta }⊢P::x:A$$\mathrm{\Gamma };\mathrm{\Delta }⊢Q::x:B$

$\mathrm{\Gamma };\mathrm{\Delta },x:A⊢P::z:C$

$\mathrm{\Gamma };\mathrm{\Delta },x:B⊢P::z:C$

The exponential and persistent-cut rules are

$\mathrm{\Gamma };\cdot ⊢P::y:A$

$\mathrm{\Gamma };\cdot ⊢!x(y).P::x:!A$

$\mathrm{\Gamma },u:A;\mathrm{\Delta }⊢P::z:C$

$\mathrm{\Gamma };\mathrm{\Delta },x:!A⊢P[x/u]::z:C$

$\mathrm{\Gamma },u:A;\mathrm{\Delta },y:A⊢P::z:C$

$\mathrm{\Gamma },u:A;\mathrm{\Delta }⊢(\nu y)u⟨y⟩.P::z:C$

$\mathrm{\Gamma };\cdot ⊢P::y:A$$\mathrm{\Gamma },u:A;\mathrm{\Delta }⊢Q::z:C$

$\mathrm{\Gamma };\mathrm{\Delta }⊢(\nu u)(!u(y).P\mid Q)::z:C$

The replicated cut requires its provider to have no linear clients. This empty-context premise is the operational reason that copies do not duplicate linear endpoints.

The unit protocol already gives a complete interaction. Define Here $P_x$ provides $x:\mathbf{1}⊸((\mathbf{1}\otimes \mathbf{1})\oplus \mathbf{1})$. The process $Q_x$ consumes that channel and provides $z:\mathbf{1}$. Every channel of type $\mathbf{1}$ is discharged by 1L, while the final $\mathbf{0}$ is typed by 1R. Put $A:=\mathbf{1}⊸((\mathbf{1}\otimes \mathbf{1})\oplus \mathbf{1})$. The complete derivation has the following spine; the displayed rule sheet determines the omitted nullary 1R leaves: $$\frac{\begin{array}{c}{\displaystyle \frac{{\displaystyle \frac{{\displaystyle \frac{\begin{array}{c}\cdot ;\cdot ⊢\mathbf{0}::m:\mathbf{1}\\ \cdot ;\cdot ⊢\mathbf{0}::x:\mathbf{1}\end{array}}{\cdot ;n:\mathbf{1}⊢R_x::x:\mathbf{1}\otimes \mathbf{1}}}}{\cdot ;n:\mathbf{1}⊢x.\mathsf{inl};R_x::x:(\mathbf{1}\otimes \mathbf{1})\oplus \mathbf{1}}}\oplus {\mathrm{R}}_1}{\cdot ;\cdot ⊢P_x::x:A}}\mathrm{\mu }\mathrm{ltimapR}\\ {\displaystyle \frac{\begin{array}{c}\cdot ;\cdot ⊢\mathbf{0}::n:\mathbf{1}\\ {\displaystyle \frac{\begin{array}{c}{\displaystyle \frac{\cdot ;m:\mathbf{1},x:\mathbf{1}⊢\mathbf{0}::z:\mathbf{1}}{\cdot ;x:\mathbf{1}\otimes \mathbf{1}⊢x(m).\mathbf{0}::z:\mathbf{1}}}\\ \cdot ;x:\mathbf{1}⊢\mathbf{0}::z:\mathbf{1}\end{array}}{\cdot ;x:(\mathbf{1}\otimes \mathbf{1})\oplus \mathbf{1}⊢x.\mathsf{case}(x(m).\mathbf{0},\mathbf{0})::z:\mathbf{1}}}\oplus \mathrm{L}\end{array}}{\cdot ;x:A⊢Q_x::z:\mathbf{1}}}\mathrm{\mu }\mathrm{ltimapL}\end{array}}{\cdot ;\cdot ⊢(\nu x)(P_x\mid Q_x)::z:\mathbf{1}}\mathrm{Cut}.$$ Here uses of 1L discharge $n,m,x:\mathbf{1}$ in the indicated leaves. Principal reductions give The interaction sends a request channel, selects the quotation branch, sends the result channel, and reaches inaction. No close or wait prefix has been silently added to the selected calculus.

Cut elimination is communication

Principal cut reductions synchronize dual rule introductions. Representative cases are Reduction is closed under restriction and parallel contexts, up to the structural congruence that reassociates and commutes independent cuts. Replicated cuts spawn one fresh linear instance per request and retain the shared server.

Proof of Theorem 58.1 — Type preservation for the selected calculus

Proof. Proceed by the reduction derivation. A principal step replaces a cut between the introduction rules for the same connective by cuts on its immediate subformulas. The displayed tensor step uses the two tensor premises and the client continuation, then applies Cut first at $y:A$ and then at $x:B$. The additive cases select an existing premise. The unit case is structural: 1L adds no process action and 1R contributes only inaction. The exponential case uses the empty linear context of $!$R; admissible renaming gives the fresh instance. Congruence cases rebuild the typing rule around the induction hypothesis. The persistent case uses Copy to spawn a fresh linear instance while retaining the replicated provider. It remains possible that the cut formula is not principal in one premise. Apply the corresponding commuting conversion to move the cut above that premise’s last rule; its derivation height decreases. The induction hypothesis then types the converted reduct, and the inverse commuting conversion restores the required process modulo structural congruence. This is why preservation is stated for reduction closed under structural congruence, rather than for the three principal contractions alone. ◻

Preservation says that a step respects the protocol. Progress needs an additional syntactic guard. Call $P$ live when, up to structural congruence, $$P\equiv (\nu \tilde{n})(\pi .Q\mid R),$$ where $\pi .Q$ is any nonreplicated guarded process: input, output, left or right selection, or branching. This excludes a process consisting only of replicated servers but includes the intermediate selection state in the worked interaction.

Proof of Theorem 58.2 — Closed progress for the selected calculus

Proof. Normalize the typing derivation by commuting cuts past rules that do not act on the cut channel. Two inversions provide the mechanism. First, if the last rule types a guarded prefix whose subject is $a$, then $a$ occurs in the typing interface with the connective introduced by that prefix. Second, a cut-free derivation of a non-live process has no nonreplicated guarded prefix. These are inductions on the displayed rule sheet; the additive cases inspect both premises and the exponential case is excluded by nonreplication.

Now suppose the normalized derivation is live. Its guard cannot be exposed at the external interface: the linear context is empty, and the offered channel has type $\mathbf{1}$, whose only right rule is 1R and has no action. The guard is therefore below a cut. Normality makes that cut principal, so its two premises end in rules introducing the same connective on the cut channel. The matching principal contraction applies. This reconstructs the source’s action-inversion and non-live-derivation lemmas for the closed instance. ◻

The source theorem also has a contextual form: a typed live process either reduces internally or exposes a labelled action whose subject is in its interface; when that interface type is $!A$, the subject is not the offered channel. Fixing the interface at empty $\mathrm{\Gamma },\mathrm{\Delta }$ and $x:\mathbf{1}$ removes the second alternative: there is no contextual subject, and $\mathbf{1}$ admits no labelled action on $x$ [CPT11]. This is a genuine global deadlock-freedom result for this proof-shaped finite calculus. It is not a theorem about arbitrary binary session programs, several independently created sessions, asynchronous queues, fairness, or termination.

Recursive protocols

The finite grammar cannot describe a server that handles arbitrarily many requests. For this section $S,T$ range over the same linear protocol sort as $A,B$, extended with variables and equi-recursive types: $$S,T::=\cdots \mid t\mid \mu t.S,\mu t.S\equiv S[\mu t.S/t].$$ A body is contractive when every occurrence of its bound variable lies strictly beneath a communication constructor—send, receive, internal choice, or external choice. In particular, $\mu t.t$ and $\mu t.\mu u.t$ are rejected. This chapter makes the additional tail-recursion restriction required by its syntactic duality: at a channel-send or channel-receive constructor, the transmitted session type is closed with respect to every surrounding recursion variable. Thus $\mu t.(A\otimes t)$ is admitted when $t\notin \mathrm{fv}(A)$, whereas $\mu t.(t\otimes \mathbf{1})$ is not. Recursive variables may still occur in continuations and choice branches.

Write $S\simeq T$ for the greatest relation generated coinductively by matching outer constructors and the two unfolding clauses $$\frac{S[\mu t.S/t]\simeq T}{\mu t.S\simeq T}\mathrm{Eq}-\mathrm{Unfold}-\mathrm{L}\frac{S\simeq T[\mu t.T/t]}{S\simeq \mu t.T}\mathrm{Eq}-\mathrm{Unfold}-\mathrm{R}.$$ For example, the tensor congruence clause requires the same closed transmitted type and related continuations. The other four constructor clauses are defined by the same outer-constructor test. Add recursive conversion explicitly: $$\frac{\begin{array}{c}\mathrm{\Gamma };\mathrm{\Delta },x:S⊢P::z:C\\ S\simeq T\end{array}}{\mathrm{\Gamma };\mathrm{\Delta },x:T⊢P::z:C}\mathrm{T}-\mathrm{Rec}-\mathrm{Conv}.$$ This rule is the only way recursive equality enters typing.

The following syntactic duality is an auxiliary endpoint view; the intuitionistic judgment above itself assigns the same cut formula to provider and client. It is defined on the linear fragment, not on the unrestricted service constructor $!A$: On the contractive, tail-recursive fragment it satisfies $$\overline{\mu t.S}=\mu t.\bar{S},\overline{\stackrel{―}{S}}=S$$ up to recursive session equality. Contractiveness makes observation of the next communication productive; closed transmitted types make the displayed syntactic duality sound.

Proof of Lemma 58.3 — Unfolding and duality

Proof. First prove the displayed substitution equation by induction on the tail-recursive formation derivation. At send and receive, the recursion substitution does not enter the closed transmitted type; it enters only the continuation, where the induction hypothesis applies. Choice uses the hypothesis branchwise; variables and $\mathbf{1}$ are immediate. Contractiveness ensures that coinductive comparison exposes one of these constructors after finitely many unfoldings.

For typing preservation, invert T-Rec-Conv. Apply theorem 58.1 to its premise and the same process step, then reapply T-Rec-Conv with the unchanged equality $S\simeq T$. If the redex is a cut exposed only after unfolding, use the substitution equation to obtain matching outer constructors, take the finite principal step, and reapply conversion to the residual continuation. Thus the new case does not assume the desired result. ◻

Contractiveness alone is insufficient. For $R=\mu t.(t\otimes \mathbf{1})$, naively dualizing the recursive syntax gives a received payload $\bar{R}$, whereas dualizing the unfolding requires the unchanged payload $R$. The two need not be equal. The source proves naive syntactic duality sound only for tail-recursive types, meaning that every message type is closed. Arbitrary contractive session types require message closure or one of the paper’s corrected duality functions [GTV20]; neither is silently folded into this local extension.

The finite rules can prescribe the kind and order of messages, but the continuation type cannot depend on the value just received. Adding such a dependency requires index equality, substitution into protocols, and a decision about whether indices are erased or communicated. Those are new proof obligations, not decorations on the finite logical rules.

Optional route.

Chapter 20.

Graded non-linear communication$\star$

This section changes calculi. It follows the final journal system of Marshall and Orchard, where a linear channel can be promoted to a shared, replicated, multicast, or graded service [MO24b]. No theorem in this section is obtained by translating the finite logical calculus in section 58.1.

The operational state distinguishes typed terms, processes, and channel configurations. Write a channel configuration as $C;\mathrm{\Delta }$, with resource environment $\mathrm{\Delta }$. Before stating progress, define $\mathsf{buffered}(C,\mathrm{\Delta })$: every runtime channel $c$ assigned $\mathsf{Chan}(\mathsf{Recv}AP)$ by $\mathrm{\Delta }$ contains at least one head value. The inductive clauses leave empty buffers available at $\mathsf{End}$ and $\mathsf{Send}$-typed channels; all other structurally paired configuration clauses are discharged without a buffer-nonemptiness premise. The syntactic predicate $\mathsf{resourceAllocator}(t)$ classifies terms whose reduction creates a channel, including reducible uses of the fork primitives. Graded promotion requires $\mathrm{\neg }\mathsf{resourceAllocator}(t)$. A lambda containing a fork is not yet an allocator because evaluation does not proceed beneath lambdas.

Each non-linear primitive carries its own side conditions:

Shared service.

$\mathsf{forkNonLinear}$ requires $\mathsf{SingleAction}$ and $\mathsf{ExactSemiring}$. The latter excludes approximate grades. The journal’s surface presentation lists five shapes: The core runtime-context definition lists only the first three shapes, whereas the surface rules and implementation also admit the two choices. This chapter uses the five-shape surface predicate and records the discrepancy.

Repeated receive.

$\mathsf{forkReplicate}$ requires $\mathsf{ReceivePrefix}$; the replicated body begins with a receive or an external offer rather than with an unrelated action.

Multicast.

$\mathsf{forkMulticast}$ requires $\mathsf{Sends}(P)$. Its channel type contains $\mathsf{Graded}nP$, the recursively defined type function that grades every payload by $n$; $\mathsf{Graded}$ is not a predicate or an additional premise.

Dropping these conditions can strand a client or allocate a different number of endpoints from the one recorded in the configuration type.

Proof of Theorem 58.4 — Journal progress and preservation card

Imported proof. The first two clauses are respectively Theorems 1 and 2 on term and global progress in Appendix C of [MO24b]; the third is Theorem 3 on preservation, stated on physical PDF p. 21 and proved in Appendix D on physical PDF pp. 46–53. Their hypotheses mention typed terms, processes, channels, and bufferedness separately. Suppressing those distinctions produces a stronger and false slogan.

A small example ladder separates the primitives. A shared logger uses $\mathsf{forkNonLinear}$ for any number of single-action clients. A pool of exactly $k$ workers additionally uses an exact natural grade and an allocator that partitions $k$. A multicast announcement uses $\mathsf{forkMulticast}$; its $\mathsf{Sends}$ witness records that its protocol sends, while the type function $\mathsf{Graded}n$ marks every payload for $n$ recipients. These programs share notation, but their side-condition proofs are different.

The pinned 2022 Granule merge supplies an exact version map. Its examples/Sessions.gr contains the PLACES-era sendVec, recvVec, and graded reusable-channel example, while frontend/tests/cases/positive/testConstraintSessions.gr exercises forkNonLinear. In that snapshot its type requires SingleAction but omits the journal rule’s ExactSemiring; this is version evidence, not a derivation of the journal rule. No pinned example or test names forkReplicate or forkMulticast; the file named replicate.gr duplicates an ordinary graded value, not a session. Therefore only the earlier shared-channel fragment has exercising examples and tests in that snapshot, although the other primitives are implemented. The journal core additionally separates term, process, and channel configurations, states buffered progress, and introduces runtime forms and side conditions that the snapshot does not certify. The final article also leaves deadlock freedom as future work. We claim neither that conjecture nor an implementation correspondence with the journal calculus. ◻

Chapter seminar

The companion Kappa corpus at artifacts/ch58-session-protocols/ encodes finite action traces, pointwise action duality, and compatibility. Its empty trace marks type $\mathbf{1}$; it is not a close or wait action. The acceptance matrix contains empty termination, tensor communication, both choices, a pre-unrolled request/answer trace, and a deliberately mismatched pair. The executable is a checker for these examples, not an implementation of the process calculus or a mechanization of either theorem card.