Dependent Session Types and Protocol-Indexed Programming

Proof. For $\mathrm{\forall }$, the provider continuation is derived under $x:\tau$ with offered type $A$. The client premise contains $y:A[M/x]$. Functional substitution in the provider derivation gives offered type $A[M/x]$, so the reduct $(\nu y)(P[M/x]\mid Q)$ is a cut on that same type. For $\mathrm{\exists }$, the provider premise already offers $A[M/x]$, and substitution in the client premise changes its assumption from $A$ to $A[M/x]$. Thus both quantifier pairs produce the displayed classifier. ◻

Proof. Weakening is induction on the functional or process derivation. The quantifier binder case alpha-renames its bound name to a name outside $\mathrm{FV}(M)\cup \mathrm{dom}(\mathrm{\Psi },{\mathrm{\Psi }}^{\prime })$.

For substitution, induct on the process derivation while using the functional substitution theorem in every term premise. In $\mathrm{\forall }$R, choose $y\notin \mathrm{FV}(M)\cup \mathrm{dom}(\mathrm{\Psi },{\mathrm{\Psi }}^{\prime })$; the induction hypothesis yields the substituted body under $y:\sigma$, and the rule rebuilds the quantified conclusion. In $\mathrm{\forall }$L, functional substitution gives the witness type and the process induction hypothesis gives the continuation with classifier $B[N/y][M/x]$. The fresh choice gives $B[M/x][N[M/x]/y]$, the classifier required by the rebuilt rule. The two existential cases use the same commutation equation, with right and left rules exchanged.

It remains to check twenty concrete rules, or eighteen rule schemas when the two branch indices are grouped. Put $$\theta =[M/x],\hat{\mathrm{\Psi }}=\mathrm{\Psi },{\mathrm{\Psi }}^{\prime }[M/x].$$ Write a superscript $(-{)}^{\theta }$ for simultaneous capture-avoiding action on channel contexts, processes, and offered types. The cases fall into the following exhaustive forms.

The nullary cases are Id, $\mathbf{1}$R, and $R. For Id, substitution changes only the classifier: $$\frac{}{\hat{\mathrm{\Psi }};{\mathrm{\Gamma }}^{\theta };y:A^{\theta }⟹[y\leftrightarrow z]::z:A^{\theta }}.$$ Rule $\mathbf{1}$R is unchanged because its linear context and offered type contain no index. In $R, functional substitution first changes its sole premise $\mathrm{\Psi },x:\tau ,{\mathrm{\Psi }}^{\prime }⊢N:\sigma$ into $\mathrm{\Psi },{\mathrm{\Psi }}^{\prime \theta }⊢N^{\theta }:{\sigma }^{\theta }$; rebuilding $R gives $[z\leftarrow N^{\theta }]::z:\mathrm{\$}{\sigma }^{\theta }$.

Four rules split a linear context. The representative $\otimes$R case is $$\frac{\hat{\mathrm{\Psi }};{\mathrm{\Gamma }}^{\theta };{\mathrm{\Delta }}_1^{\theta }⟹P^{\theta }::y:A^{\theta }\hat{\mathrm{\Psi }};{\mathrm{\Gamma }}^{\theta };{\mathrm{\Delta }}_2^{\theta }⟹Q^{\theta }::z:B^{\theta }}{\hat{\mathrm{\Psi }};{\mathrm{\Gamma }}^{\theta };{\mathrm{\Delta }}_1^{\theta },{\mathrm{\Delta }}_2^{\theta }⟹(\nu y)z⟨y⟩.(P^{\theta }\mid Q^{\theta })::z:A^{\theta }\otimes B^{\theta }}.$$ The induction hypotheses supply its two premises. Since $\theta$ changes classifiers but no channel name, $\mathrm{dom}({\mathrm{\Delta }}_1^{\theta })\cap \mathrm{dom}({\mathrm{\Delta }}_2^{\theta })=\varnothing$. Rule $⊸$L is this schema with the first result channel sent to the second premise. Rule Cut replaces the displayed output constructor by $(\nu y)(P^{\theta }\mid Q^{\theta })$. Rule Cut${}^{!}$ has an empty first linear context and puts its cut formula in the persistent context of the second premise. Functional substitution preserves both facts, so those three rules rebuild without an additional structural principle.

Two rules have two premises with the same linear context. For R, the two induction hypotheses have exactly ${\mathrm{\Delta }}^{\theta }$ and rebuild $z.\mathsf{case}(P^{\theta },Q^{\theta })$. For $\oplus$L, they have ${\mathrm{\Delta }}^{\theta },y:A^{\theta }$ and ${\mathrm{\Delta }}^{\theta },y:B^{\theta }$, respectively, and rebuild $y.\mathsf{case}(P^{\theta },Q^{\theta })$. Thus neither case silently turns a shared context into a split one.

The remaining unary cases are exact instances of $$\begin{array}{}\text{(}U\text{)}& \frac{\hat{\mathrm{\Psi }};{\mathrm{\Gamma }}^{\theta };(\mathrm{\Delta },y:A{)}^{\theta }⟹P^{\theta }::z:C^{\theta }}{\hat{\mathrm{\Psi }};{\mathrm{\Gamma }}^{\theta };(\mathrm{\Delta },y:F(A){)}^{\theta }⟹F_y(P^{\theta })::z:G(A,C{)}^{\theta }},\end{array}$$ where $F,F_y,G$ are the constructors printed on the corresponding rule. The exact instances are as follows. Rule $\mathbf{1}$L deletes the unused $y:\mathbf{1}$ from the premise. Rule $\otimes$L replaces premise entries $w:A,y:B$ by the one conclusion entry $y:A\otimes B$. Rule $⊸$R abstracts the premise entry $y:A$ and offers $A⊸B$. Rules L${}_1$ and L${}_2$ select $A$ and $B$, respectively; rules $\oplus$R${}_1$ and $\oplus$R${}_2$ make the corresponding offered choice. Because substitution commutes with each type constructor, for example $(A\otimes B{)}^{\theta }=A^{\theta }\otimes B^{\theta }$, each conclusion is the required instance of (U).

For !R, the induction hypothesis retains the empty linear context. For !L, it changes the persistent premise entry $u:A$ to $u:A^{\theta }$ and the linear conclusion entry $y:!A$ to $y:!A^{\theta }$. The Copy case changes both its persistent $u:A$ and fresh linear $y:A$ entries to $A^{\theta }$; the side condition that $y$ is fresh is preserved because $\theta$ introduces no channel names. Finally, $L is alpha-renamed so that its channel name $y$ is different from the substituted functional variable $x$. Its induction hypothesis changes the premise functional entry from $y:\sigma$ to $y:{\sigma }^{\theta }$, and $L rebuilds the conclusion entry $y:\mathrm{\$}{\sigma }^{\theta }$. These nullary, split, same-context binary, unary, and four quantifier cases cover every rule in definition 102.1, definition 102.3. ◻

Proof. By cases on the cut formula $A$. Each nonpersistent case exhibits the step and then the rebuilt derivation; the conclusion is the same in every case, so only the cut structure changes. The persistent case exhibits first the proof conversion and then the step triggered by Copy.

For $\mathrm{\forall }y:\tau .B$, the provider receives a term by $\mathrm{\forall }$R and the client sends one by $\mathrm{\forall }$L. lemma 102.5 gives both residual classifiers as $B[M/y]$, so the reduct is one cut on $B[M/y]$. For $\mathrm{\exists }$ the polarities are exchanged and the same lemma applies.

For $A_1\otimes A_2$, the provider is $(\nu y)x⟨y⟩.(P_1\mid P_2)$ with $P_1::y:A_1$ and $P_2::x:A_2$, and the client is $x(y).Q$ with $y:A_1,x:A_2$ among its assumptions. The step is $$(\nu x)((\nu y)x⟨y⟩.(P_1\mid P_2)\mid x(y).Q)⟶(\nu x)(P_2\mid (\nu y)(P_1\mid Q)).$$ Read the reduct carefully, because it is not what a substitution lemma would produce. The name $x$ survives: the inner cut composes $P_1$ and $Q$ on the fresh $y$ at type $A_1$, and the outer cut still composes $P_2$ and that composite on $x$, now at the residual type $A_2$. One cut at $A_1\otimes A_2$ has become two, at $A_1$ and at $A_2$; the channel is consumed only when its type is finally $\mathbf{1}$. $A_1⊸A_2$ is the same step with provider and client exchanged.

For $A_1\oplus A_2$, the selection prefix $x.\mathsf{inl}$ meets $x.\mathsf{case}$ and the reduct discards the unselected branch, leaving one cut on $A_1$ along the same $x$; exchanges the two sides. For $\mathbf{1}$ the provider is $\mathbf{0}$ and the client continues, so the cut disappears and $x$ is consumed — this is the one case in which it is. For $\mathrm{\$}\tau$ the delayed functional substitution of definition 102.2 fires and $x$ changes sort from a linear channel to a functional assumption.

For $!B$, the principal proof reduction first turns the ordinary cut against !L into the persistent cut $$(\nu u)(!u(y).P_0\mid Q),$$ where $P_0::y:B$ has no linear assumptions and $Q$ uses $u:B$ only through Copy. A particular copy has process $(\nu v)u⟨v⟩.R$. Scope extrusion exposes the root step $$u⟨v⟩.R\mid !u(y).P_0⟶R\mid P_0[v/y]\mid !u(y).P_0.$$ The request channel $v$ is linear and the resulting cut formula is the immediate subformula $B$. The replicated input remains available, but its contraction is confined to the persistent declaration $u:B$ in $\mathrm{\Gamma }$; no declaration of ${\mathrm{\Delta }}_1,{\mathrm{\Delta }}_2$ is copied.

In every case the conclusion retains the union ${\mathrm{\Delta }}_1,{\mathrm{\Delta }}_2$, and disjointness is what lets the two premises be recombined without a name clash. ◻

Proof. Induct on the typing derivation. A principal cut is lemma 102.7, whose statement already gives the rebuilt derivation at the same conclusion. The dependent quantifier cases of that lemma rest on lemma 102.5, and term passing additionally uses lemma 102.6 to move $M$ into the residual classifier. A reduction under parallel composition or restriction rebuilds the induction hypothesis with the same linear split. Structural congruence uses exchange, alpha-renaming, and the fact that restriction extrusion preserves the disjointness side condition. The persistent cut case invokes contraction only in $\mathrm{\Gamma }$, never in $\mathrm{\Delta }$. These cases cover the operational rules of definition 102.2, so the induction proves preservation for the displayed calculus. ◻

Proof. We first prove the contextual claim used by the closed theorem. If $\mathrm{\Psi };\mathrm{\Gamma };\mathrm{\Delta }⟹R::z:C$ and $\mathsf{live}(R)$, then at least one of the following conclusions is derivable up to structural congruence:

1. $R⟶R^{\prime }$ for some process $R^{\prime }$;

2. $R$ exposes a prefix whose subject is $z$, a channel in $\mathrm{\Delta }$, or, when $C=!A$, a persistent channel in $\mathrm{\Gamma }$;

3. $R$ is a forwarding process $[x\leftrightarrow z]$ with $x\in \mathrm{\Delta }$, or a functional substitution $[x\leftarrow M]$ whose free functional variables lie in $\mathrm{\Psi }$.

Prove the claim by induction on the last typing rule. An introduction rule for , or $\mathrm{\forall }$ exposes the constructor prescribed by that rule, so clause 2 holds. A forwarding or functional-substitution rule gives clause 3. Exchange and alpha-renaming preserve the selected clause because they change neither a prefix subject nor the free-channel set.

It remains to check the two cut families. Write the cut as $(\nu x)(R_1\mid R_2)$, with disjoint linear contexts in its two premises. Apply the induction hypothesis to every live premise. If one premise reduces, compatible closure reduces the cut. If the two premises expose dual actions on $x$, the corresponding root rule in definition 102.2 reduces the cut. This includes channel passing, label selection, termination, and the two dependent-quantifier cases. In a dependent communication, the residual classifiers are equal by lemma 102.5; functional payload communication also uses lemma 102.6. If no exposed action has subject $x$, restriction hides $x$ and the remaining exposed action has a free subject belonging to the conclusion context. A forwarding or functional-substitution form at $x$ contracts by the appropriate cut root; one on a different subject survives restriction and gives clause 3. A persistent cut uses the same analysis, except that contraction occurs only in $\mathrm{\Gamma }$. These cases exhaust the typing rules and prove the contextual claim.

Apply the claim to the theorem’s derivation. The assumed-channel contexts $\mathrm{\Gamma }$ and $\mathrm{\Delta }$ are empty, so clauses 2 and 3 cannot mention an assumed channel or a free functional payload. The offered channel has type $\mathbf{1}$; its only introduction is the inactive termination process, which contradicts $\mathsf{live}(P)$. Thus clause 2 is impossible on the offered channel as well. Clause 3 is impossible in the empty contexts. Clause 1 remains, and supplies $Q$ with $P⟶Q$. ◻