Typed potentials and session protocols

Chapter 57: polynomial AARA

The fixed resource metric is $$K^{\mathsf{pair}}=K^{\mathsf{cons}}=1,K_i^{\mathsf{c}}=0\text{otherwise}.$$ Evaluation is terminating big-step $V,H{⊢}_{q^{\prime }}^{q}e\Downarrow v,H^{\prime }$ and typing is $\mathrm{\Sigma };\mathrm{\Gamma }{⊢}_{p^{\prime }}^{p}e:A$. Degree-$d$ list potential uses $$\phi (n,\overrightarrow{p})=\sum _{i=1}^d{p}_i(\genfrac{}{}{0ex}{}{n}{i}),\mathsf{C}(p_1,\dots ,p_d)=(p_1+p_2,\dots ,p_{d-1}+p_d,p_d).$$ The identity $\phi (n+1,\overrightarrow{p})=p_1+\phi (n,\mathsf{C}\overrightarrow{p})$ drives both list construction and matching. The evaluation rules used by the soundness proof are

$V(x_1)=v_1$$V(x_2)=v_2$$l\notin \mathrm{dom}(H)$

$V,H{⊢}_q^{q+K^{\mathsf{pair}}}(x_1,x_2)\Downarrow l,H[l\mapsto (v_1,v_2)]$

$V(x_h)=v_h$$V(x_t)=v_t$$l\notin \mathrm{dom}(H)$

$V,H{⊢}_q^{q+K^{\mathsf{cons}}}\mathsf{cons}(x_h,x_t)\Downarrow l,H[l\mapsto (v_h,v_t)]$

$V,H{⊢}_{q_2}^{q_1-K_1^{\mathsf{let}}}{e}_1\Downarrow v_1,H_1$$V[x\mapsto v_1],H_1{⊢}_{q_3+K_3^{\mathsf{let}}}^{q_2-K_2^{\mathsf{let}}}{e}_2\Downarrow v_2,H_2$

$V,H{⊢}_{q_3}^{q_1}\mathsf{let}x=e_1\mathsf{in}{e}_2\Downarrow v_2,H_2$

$[y_1^f\mapsto v_1,\dots ,y_k^f\mapsto v_k],H{⊢}_{u^{\prime }+K_2^{\mathsf{app}}}^{u-K_1^{\mathsf{app}}}{e}_f\Downarrow v,H^{\prime }$

$V,H{⊢}_{u^{\prime }}^{u}f(x_1,\dots ,x_k)\Downarrow v,H^{\prime }$

List construction and the structural typing rules are

$\overrightarrow{p}=(p_1,\dots ,p_d)$

$\mathrm{\Sigma };x_h:A,x_t:L^{\mathsf{C}(\overrightarrow{p})}(A){⊢}_0^{p_1+K^{\mathsf{cons}}}\mathsf{cons}(x_h,x_t):L^{\overrightarrow{p}}(A)$

$\mathrm{\Sigma };{\mathrm{\Gamma }}_1{⊢}_p^{q-K_1^{\mathsf{let}}}{e}_1:A$$\mathrm{\Sigma };{\mathrm{\Gamma }}_2,x:A{⊢}_{q^{\prime }+K_3^{\mathsf{let}}}^{p-K_2^{\mathsf{let}}}{e}_2:B$

$\mathrm{\Sigma };{\mathrm{\Gamma }}_1,{\mathrm{\Gamma }}_2{⊢}_{q^{\prime }}^q\mathsf{let}x=e_1\mathsf{in}{e}_2:B$

$\mathrm{\Sigma };\mathrm{\Gamma },x:A_1,y:A_2{⊢}_{q^{\prime }}^{q}e:B$$\mathsf{share}(A;A_1,A_2)$

$\mathrm{\Sigma };\mathrm{\Gamma },z:A{⊢}_{q^{\prime }}^{q}e[z/x,z/y]:B$

$\mathrm{\Sigma };\mathrm{\Gamma }{⊢}_{q^{\prime }}^{q}e:B$$x\notin \mathrm{dom}(\mathrm{\Gamma })$

$\mathrm{\Sigma };\mathrm{\Gamma },x:A{⊢}_{q^{\prime }}^{q}e:B$

Function application, empty lists, subtyping, and relaxation are

$\mathrm{\Sigma }(f)=(A_1,\dots ,A_k)\stackrel{q/q^{\prime }}{\to }A$

$\mathrm{\Sigma };x_1:A_1,\dots ,x_k:A_k{⊢}_{q^{\prime }-K_2^{\mathsf{app}}}^{q+K_1^{\mathsf{app}}}f(x_1,\dots ,x_k):A$

$A\mathsf{type}$

$\mathrm{\Sigma };\varnothing {⊢}_0^{K^{\mathsf{nil}}}[]:L^{\overrightarrow{0}}(A)$

$\mathrm{\Sigma };\mathrm{\Gamma },x:A{⊢}_{q^{\prime }}^{q}e:B$

$\mathrm{\Sigma };\mathrm{\Gamma },x:A_0{⊢}_{q^{\prime }}^{q}e:B$

$\mathrm{\Sigma };\mathrm{\Gamma }{⊢}_{q^{\prime }}^{q}e:B$

$\mathrm{\Sigma };\mathrm{\Gamma }{⊢}_{q^{\prime }}^{q}e:B_0$

$\mathrm{\Sigma };\mathrm{\Gamma }{⊢}_{p^{\prime }}^{p}e:B$$q\ge p$$q-p\ge q^{\prime }-p^{\prime }$

$\mathrm{\Sigma };\mathrm{\Gamma }{⊢}_{q^{\prime }}^{q}e:B$

Sharing splits coefficients additively; affine weakening adds an unused assumption; same-shape subtyping may only discard potential. Soundness assumes a well-formed stack and heap, an existing terminating evaluation, a typing derivation, and nonnegative slack. It returns the same value and heap with residual resource at least the output potential plus the promised residual annotation and slack.

Chapter 21: finite logical sessions

The selected provider judgment is $\mathrm{\Gamma };\mathrm{\Delta }⊢P::z:A$, with unrestricted $\mathrm{\Gamma }$, linear $\mathrm{\Delta }$, and pairwise-disjoint interface names. The type constructors follow the intuitionistic-linear right/left rules. The unit, tensor, implication, and cut rules are

$\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$

Cut connects exactly one provider to one client. Replicated provision has an empty linear context. Principal cut reductions synchronize send/receive and selection/branch. The unit has no communication action: 1R is inaction and 1L leaves its process unchanged. The additive rules are

$\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$

Replication is governed by

$\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$

Preservation retains the same judgment. Closed progress requires $\cdot ;\cdot ⊢P::x:\mathbf{1}$ and a live nonreplicated top-level prefix. The local recursive extension is both contractive and tail-recursive: every transmitted session type is closed with respect to the surrounding recursion variables. Naive syntactic duality commutes with unfolding only on that fragment; arbitrary contractive types require message closure or another corrected duality. The recursive equality and typing closure rules are

$S[\mu t.S/t]\simeq T$

$\mu t.S\simeq T$

$S\simeq T[\mu t.T/t]$

$S\simeq \mu t.T$

$\mathrm{\Gamma };\mathrm{\Delta },x:S⊢P::z:C$$S\simeq T$

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

The separate graded journal card first defines $\mathsf{buffered}(C,\mathrm{\Delta })$. It says exactly that every runtime channel typed $\mathsf{Chan}(\mathsf{Recv}AP)$ has a head value. Term/global progress and post-context preservation require the paper’s separately typed term, process, and channel configurations. Primitive rules use SingleAction and ExactSemiring, ReceivePrefix, or Sends where displayed; $\mathsf{Graded}nP$ is a protocol type function in the multicast channel type, not a predicate premise.

Chapter 59: repaired MPST and Pirouette

The repaired global/local types have explicit queue addresses. Full projection is partial. A global type is coherent exactly when it is projectable, linear, and coinductively unstuck: every relaxed barb has a true global transition to another unstuck type. Local and decomposed local/queue environments inherit coherence through full projection and a path decomposition. Subject reduction allows the coherent global specification either to remain fixed or to make one labelled interaction step, and yields a possibly changed process typing environment and queue specification. Linearity closes the input- and output-dependency relations by

$\mathsf{IO}(a_0,a_1)$$\mathsf{InDep}(a_1,\dots ,a_n)$

$\mathsf{InDep}(a_0,a_1,\dots ,a_n)$

$\mathsf{IO}(a_0,a_1)\vee \mathsf{OO}(a_0,a_1)$

$\mathsf{OutDep}(a_0,a_1)$

$\mathsf{IO}(a_0,a_1)\vee \mathsf{OO}(a_0,a_1)$$\mathsf{OutDep}(a_1,\dots ,a_n)$

$\mathsf{OutDep}(a_0,a_1,\dots ,a_n)$

The process and queue interfaces are connected by

$\mathrm{\Gamma }⊢e:U$$\mathrm{\Gamma }{⊢}_{D}P{▹}_C\mathrm{\Delta },s^p:T;Q$

$\mathrm{\Gamma }{⊢}_D{s}^p[k]!⟨e⟩;P{▹}_C\mathrm{\Delta },s^p:!k⟨U⟩.T;Q$

$\mathrm{\Gamma }⊢v:U$$\mathrm{\Gamma }{⊢}_{D}s[k]::\tilde{h}{▹}_C\mathrm{\Delta };Q$

$\mathrm{\Gamma }{⊢}_{D}s[k]::(\tilde{h}\cdot p!v){▹}_C\mathrm{\Delta };Q\cdot (k,p,U)$

Communication safety follows; progress, deadlock freedom, orphan freedom, fairness, and liveness do not.

Pirouette is a separate synchronous calculus parameterized by a local language with decidable location equality, substitution laws, closed values, unique typing and structural/substitution rules. Relative progress also needs Boolean inversion and local progress; relative preservation needs local preservation. The choreography semantics uses block sets for out-of-order steps and synchronizes higher-order calls globally. Endpoint projection uses partial merge. Global projection soundness assumes $\mathrm{LN}(C)\subseteq L\ne \varnothing$. The reached-projection deadlock corollary separately assumes $\mathsf{PirExprClosed}(C)$, the displayed choreography typing judgment, and a choreography type system with progress and preservation.