Erasure, dependent protocols, effects, specifications, and partiality

Graded erasure and extraction

Usage is a judgment independent of typing. Its function fragment is

$e_i▸x_i$

$\gamma ,p▸t$

$\gamma ▸{\lambda }^{p}t$

$\gamma ▸t$$\delta ▸u$

$\gamma +p\delta ▸t{}^{p}u$

Natural-number elimination uses

${\gamma }_z▸z$${\gamma }_s,p,r▸s$${\gamma }_n▸n$$\delta ,q▸A$

${\mathsf{nr}}_{p,r}({\gamma }_z,{\gamma }_s,{\gamma }_n)▸{\mathsf{natrec}}_{p,r}^q(A;z;s;n)$

Simultaneous substitution replaces a usage row by matrix multiplication: if every row $e_i\mathrm{\Psi }$ resources $\sigma (i)$, then $\gamma ▸t$ entails $\gamma \mathrm{\Psi }▸t[\sigma ]$. The natural-recursion demand is ${\mathsf{nr}}_{p,r}(q_z,q_s,q_n)$, governed by the five scalar laws The first three lines are NR-Base, NR-Step, and NR-Mono. The last two are NR-Right and NR-Interchange. All five lift pointwise to usage contexts. At nonzero grade, extraction retains lambdas and applications. At grade zero it uses $$({\lambda }^{0}t{)}^{\bullet }=t^{\bullet }[\circlearrowleft /x],(t{}^{0}u{)}^{\bullet }=t^{\bullet }.$$ An erased weak-pair match is admitted only at the match grades selected by $\mathsf{Prodrec}$; the open-context restriction in theorem 101.11 remains a theorem hypothesis.

Dependent session quantifiers

For a total functional judgment $\mathrm{\Psi }⊢M:\tau$, the four added rules are

$\mathrm{\Psi },x:\tau ;\mathrm{\Gamma };\mathrm{\Delta }⟹P::z:A$

$\mathrm{\Psi };\mathrm{\Gamma };\mathrm{\Delta }⟹z(x).P::z:\mathrm{\forall }x:\tau .A$

$\mathrm{\Psi }⊢M:\tau$$\mathrm{\Psi };\mathrm{\Gamma };\mathrm{\Delta },y:A[M/x]⟹Q::z:C$

$\mathrm{\Psi };\mathrm{\Gamma };\mathrm{\Delta },y:\mathrm{\forall }x:\tau .A⟹y⟨M⟩.Q::z:C$

and

$\mathrm{\Psi }⊢M:\tau$$\mathrm{\Psi };\mathrm{\Gamma };\mathrm{\Delta }⟹P::z:A[M/x]$

$\mathrm{\Psi };\mathrm{\Gamma };\mathrm{\Delta }⟹z⟨M⟩.P::z:\mathrm{\exists }x:\tau .A$

$\mathrm{\Psi },x:\tau ;\mathrm{\Gamma };\mathrm{\Delta },y:A⟹Q::z:C$

$\mathrm{\Psi };\mathrm{\Gamma };\mathrm{\Delta },y:\mathrm{\exists }x:\tau .A⟹y(x).Q::z:C$

A functional value can also cross the process boundary through

$\mathrm{\Psi }⊢M:\tau$

$\mathrm{\Psi };\mathrm{\Gamma };\cdot ⟹[z\leftarrow M]::z:\mathrm{\$}\tau$

$\mathrm{\Psi },x:\tau ;\mathrm{\Gamma };\mathrm{\Delta }⟹P::z:C$

$\mathrm{\Psi };\mathrm{\Gamma };\mathrm{\Delta },x:\mathrm{\$}\tau ⟹P::z:C$

A principal quantifier cut substitutes the communicated functional term in the receiving continuation. Functional substitution changes all protocol indices; linear channel substitution composes processes and requires a disjoint split of the linear channel context.

Dependent call-by-push-value

The value/computation boundary has

$\mathrm{\Gamma }{⊢}^{\mathsf{v}}V:A$

$\mathrm{\Gamma }{⊢}^{\mathsf{c}}\mathsf{return}V:FA$

$\mathrm{\Gamma }{⊢}^{\mathsf{c}}M:\underset{―}{B}$

$\mathrm{\Gamma }{⊢}^{\mathsf{v}}\mathsf{thunk}M:U\underset{―}{B}$

$\mathrm{\Gamma }{⊢}^{\mathsf{v}}V:U\underset{―}{B}$

$\mathrm{\Gamma }{⊢}^{\mathsf{c}}\mathsf{force}V:\underset{―}{B}$

The dependent Kleisli extension is preceded by the nondependent sequencing rule

$\mathrm{\Gamma }{⊢}^{\mathsf{c}}M:FA$$\mathrm{\Gamma },x:A{⊢}^{\mathsf{c}}N:\underset{―}{B}$$x\notin \mathrm{FV}(\underset{―}{B})$

$\mathrm{\Gamma }{⊢}^{\mathsf{c}}M\mathsf{to}x\mathsf{in}N:\underset{―}{B}$

The plus rule is

$\mathrm{\Gamma },z:UFA,{\mathrm{\Gamma }}^{\prime }⊢\underset{―}{B}\mathsf{ctype}$$\mathrm{\Gamma }{⊢}^{\mathsf{c}}M:FA$$\mathrm{\Gamma },x:A,{\mathrm{\Gamma }}^{\prime }[\mathsf{tr}x/z]{⊢}^{\mathsf{c}}N:\underset{―}{B}[\mathsf{tr}x/z]$

$\mathrm{\Gamma },{\mathrm{\Gamma }}^{\prime }[\mathsf{thunk}M/z]{⊢}^{\mathsf{c}}M\mathsf{to}x\mathsf{in}N:\underset{―}{B}[\mathsf{thunk}M/z]$

where $\mathsf{tr}x=\mathsf{thunk}(\mathsf{return}x)$. Its beta root is $(\mathsf{return}V)\mathsf{to}x\mathsf{in}N{⇝}_{0}N[V/x]$. A step of $M$ is type preserving at this rule only when the classifier has the printed thunkability equation.

Dijkstra computation types

The generated state transformer operations are For state with exceptions, the distinctive failure and handler clauses are Computation types use generated transformers through

$\mathrm{\Gamma }⊢V:A$

$\mathrm{\Gamma }⊢\mathsf{return}V:\mathsf{M}A({\mathsf{return}}^{\mathsf{wp}}V)$

$\mathrm{\Gamma }⊢M:\mathsf{M}Aw$$\mathrm{\Gamma },x:A⊢N:\mathsf{M}Bk(x)$

$\mathrm{\Gamma }⊢M\mathsf{to}x\mathsf{in}N:\mathsf{M}B({\mathsf{bind}}^{\mathsf{wp}}(w,k))$

and weakening a specification uses

$\mathrm{\Gamma }⊢M:\mathsf{M}Aw$$\mathrm{\Gamma }⊢\mathrm{\forall }p.w^{\prime }(p)\Rightarrow w(p)$

$\mathrm{\Gamma }⊢M:\mathsf{M}A{w}^{\prime }$

Partial elements

For $A^{\nu }$, convergence and guarded sequencing are generated by

$⟨a⟩\Downarrow a$

$x\Downarrow a$

$▹x\Downarrow a$

$$⟨a⟩\gg =f=f(a),(▹x)\gg =f=▹(x\gg =f).$$ Weak equality and the approximation order are $$x{=}_{\nu }y:=\mathrm{\forall }a.x\Downarrow a\leftrightarrow y\Downarrow a,f⊑g:=\mathrm{\forall }a,b.f(a)\Downarrow b\Rightarrow g(a)\Downarrow b.$$ The monad laws hold at ${=}_{\nu }$, not at raw constructor equality.

Graded erasure: additional formation, equality, usage, and dynamics

Together with the graded-erasure card immediately above, the rules below record the noninherited part of the signature in definition 101.2, definition 101.3, definition 101.4, definition 101.5, definition 101.9. Appendix A does not repeat the binder, congruence, and constructor schemas displayed in those definitions; those point-of-use displays are the complete signature.

$⊢ϵ$

$x_0:A[\uparrow ]\in \mathrm{\Gamma }.A$

$x_i:A\in \mathrm{\Gamma }$

$x_{i+1}:A[\uparrow ]\in \mathrm{\Gamma }.B$

$\mathrm{\Gamma }⊢A:\mathsf{U}$

$\mathrm{\Gamma }⊢A$

$\mathrm{\Gamma }.A⊢B$

$\mathrm{\Gamma }⊢{\mathrm{\Pi }}_p^{q}AB$

$\mathrm{\Gamma }.A⊢B$

$\mathrm{\Gamma }⊢{\mathrm{\Sigma }}_k^{q}AB$

$⊢\mathrm{\Gamma }$

$\mathrm{\Gamma }⊢\mathsf{N}:\mathsf{U}$

$⊢\mathrm{\Gamma }$

$\mathrm{\Gamma }⊢\mathrm{\perp }:\mathsf{U}$

$\mathrm{\Gamma }⊢A:\mathsf{U}$$\mathrm{\Gamma }.A⊢B:\mathsf{U}$

$\mathrm{\Gamma }⊢{\mathrm{\Pi }}_p^{q}AB:\mathsf{U}$

$\mathrm{\Gamma }⊢A:\mathsf{U}$$\mathrm{\Gamma }.A⊢B:\mathsf{U}$

$\mathrm{\Gamma }⊢{\mathrm{\Sigma }}_k^{q}AB:\mathsf{U}$

$\mathrm{\Gamma }.{\mathrm{\Sigma }}_{\otimes }^{q^{\prime }}AB⊢C$$\mathrm{\Gamma }⊢t:{\mathrm{\Sigma }}_{\otimes }^{q^{\prime }}AB$$\mathrm{\Gamma }.A.B⊢u:C[{\uparrow }^2,(x_1,x_0{)}_{\otimes }]$

$\mathrm{\Gamma }⊢{\mathsf{prodrec}}_r^q(C;t;u):C[t]$

$\mathrm{\Gamma }⊢A$$\mathrm{\Gamma }⊢t:\mathrm{\perp }$

$\mathrm{\Gamma }⊢{\mathsf{emptyrec}}^p(A;t):A$

$\mathrm{\Gamma }⊢z:A[\mathsf{zero}]$$\mathrm{\Gamma }.\mathsf{N}.A⊢s:A[{\uparrow }^2,\mathsf{suc}{x}_1]$$\mathrm{\Gamma }⊢n:\mathsf{N}$

$\mathrm{\Gamma }⊢{\mathsf{natrec}}_{p,r}^q(A;z;s;n):A[n]$

$\mathrm{\Gamma }⊢A=B:\mathsf{U}$

$\mathrm{\Gamma }⊢A=B$

$\mathrm{\Gamma }⊢A$

$\mathrm{\Gamma }⊢A=A$

$\mathrm{\Gamma }⊢A=B$

$\mathrm{\Gamma }⊢B=A$

$\mathrm{\Gamma }⊢A=B$$\mathrm{\Gamma }⊢B=C$

$\mathrm{\Gamma }⊢A=C$

$\mathrm{\Gamma }⊢A=A^{\prime }$$\mathrm{\Gamma }.A⊢B=B^{\prime }$

$\mathrm{\Gamma }⊢{\mathrm{\Pi }}_p^{q}AB={\mathrm{\Pi }}_p^q{A}^{\prime }{B}^{\prime }$

$\mathrm{\Gamma }⊢A=A^{\prime }$$\mathrm{\Gamma }.A⊢B=B^{\prime }$

$\mathrm{\Gamma }⊢{\mathrm{\Sigma }}_k^{q}AB={\mathrm{\Sigma }}_k^q{A}^{\prime }{B}^{\prime }$

$\mathrm{\Gamma }⊢t:A$

$\mathrm{\Gamma }⊢t=t:A$

$\mathrm{\Gamma }⊢A$$\mathrm{\Gamma }⊢t=u:A$

$\mathrm{\Gamma }⊢u=t:A$

$\mathrm{\Gamma }⊢t=u:A$$\mathrm{\Gamma }⊢u=v:A$

$\mathrm{\Gamma }⊢t=v:A$

$\mathrm{\Gamma }⊢t=u:A$$\mathrm{\Gamma }⊢A=B$

$\mathrm{\Gamma }⊢t=u:B$

$\mathrm{\Gamma }⊢A=A^{\prime }:\mathsf{U}$$\mathrm{\Gamma }.A⊢B=B^{\prime }:\mathsf{U}$

$\mathrm{\Gamma }⊢{\mathrm{\Pi }}_p^{q}AB={\mathrm{\Pi }}_p^q{A}^{\prime }{B}^{\prime }:\mathsf{U}$

$\mathrm{\Gamma }⊢A=A^{\prime }:\mathsf{U}$$\mathrm{\Gamma }.A⊢B=B^{\prime }:\mathsf{U}$

$\mathrm{\Gamma }⊢{\mathrm{\Sigma }}_k^{q}AB={\mathrm{\Sigma }}_k^q{A}^{\prime }{B}^{\prime }:\mathsf{U}$

$\mathrm{\Gamma }⊢t=t^{\prime }:{\mathrm{\Pi }}_p^{q}AB$$\mathrm{\Gamma }⊢u=u^{\prime }:A$

$\mathrm{\Gamma }⊢t{}^{p}u=t^{\prime }{}^p{u}^{\prime }:B[u]$

$\mathrm{\Gamma }.A⊢B$$\mathrm{\Gamma }.A⊢t:B$$\mathrm{\Gamma }⊢u:A$

$\mathrm{\Gamma }⊢({\lambda }^{p}t){}^{p}u=t[u]:B[u]$

$\mathrm{\Gamma }.A⊢B$$\mathrm{\Gamma }⊢t:{\mathrm{\Pi }}_p^{q}AB$$\mathrm{\Gamma }⊢u:{\mathrm{\Pi }}_p^{q}AB$$\mathrm{\Gamma }.A⊢t[\uparrow ]{}^p{x}_0=u[\uparrow ]{}^p{x}_0:B$

$\mathrm{\Gamma }⊢t=u:{\mathrm{\Pi }}_p^{q}AB$

$\mathrm{\Gamma }.A⊢B$$\mathrm{\Gamma }⊢t:A$$\mathrm{\Gamma }⊢u:B[t]$

$\mathrm{\Gamma }.A⊢B$

$\mathrm{\Gamma }⊢\mathsf{fst}t=\mathsf{fst}u:A$

$\mathrm{\Gamma }.A⊢B$$\mathrm{\Gamma }⊢t:A$$\mathrm{\Gamma }⊢u:B[t]$

$\mathrm{\Gamma }.A⊢B$

$\mathrm{\Gamma }⊢\mathsf{snd}t=\mathsf{snd}u:B[\mathsf{fst}t]$

$\mathrm{\Gamma }.A⊢B$$\mathrm{\Gamma }⊢\mathsf{fst}t=\mathsf{fst}u:A$$\mathrm{\Gamma }⊢\mathsf{snd}t=\mathsf{snd}u:B[\mathsf{fst}t]$

$\mathrm{\Gamma }.A⊢B$$\mathrm{\Gamma }⊢t=t^{\prime }:A$$\mathrm{\Gamma }⊢u=u^{\prime }:B[t]$

$\mathrm{\Gamma }⊢(t,u{)}_k=(t^{\prime },u^{\prime }{)}_k:{\mathrm{\Sigma }}_k^{q}AB$

$\mathrm{\Gamma }.{\mathrm{\Sigma }}_{\otimes }^{q^{\prime }}AB⊢C$$\mathrm{\Gamma }⊢t:A$$\mathrm{\Gamma }⊢t^{\prime }:B[t]$$\mathrm{\Gamma }.A.B⊢u:C[{\uparrow }^2,(x_1,x_0{)}_{\otimes }]$

$\mathrm{\Gamma }⊢{\mathsf{prodrec}}_r^q(C;(t,t^{\prime }{)}_{\otimes };u)=u[t,t^{\prime }]:C[(t,t^{\prime }{)}_{\otimes }]$

$\mathrm{\Gamma }.{\mathrm{\Sigma }}_{\otimes }^{q^{\prime }}AB⊢C=C^{\prime }$$\mathrm{\Gamma }⊢t=t^{\prime }:{\mathrm{\Sigma }}_{\otimes }^{q^{\prime }}AB$$\mathrm{\Gamma }.A.B⊢u=u^{\prime }:C[{\uparrow }^2,(x_1,x_0{)}_{\otimes }]$

$\mathrm{\Gamma }⊢{\mathsf{prodrec}}_r^q(C;t;u)={\mathsf{prodrec}}_r^q(C^{\prime };t^{\prime };u^{\prime }):C[t]$

$\mathrm{\Gamma }⊢z:A[\mathsf{zero}]$$\mathrm{\Gamma }.\mathsf{N}.A⊢s:A[{\uparrow }^2,\mathsf{suc}{x}_1]$

$\mathrm{\Gamma }⊢{\mathsf{natrec}}_{p,r}^q(A;z;s;\mathsf{zero})=z:A[\mathsf{zero}]$

$\mathrm{\Gamma }⊢z:A[\mathsf{zero}]$$\mathrm{\Gamma }.\mathsf{N}.A⊢s:A[{\uparrow }^2,\mathsf{suc}{x}_1]$$\mathrm{\Gamma }⊢n:\mathsf{N}$

$\mathrm{\Gamma }⊢{\mathsf{natrec}}_{p,r}^q(A;z;s;\mathsf{suc}n)=s[n,{\mathsf{natrec}}_{p,r}^q(A;z;s;n)]:A[\mathsf{suc}n]$

$\mathrm{\Gamma }⊢t=u:\mathsf{N}$

$\mathrm{\Gamma }⊢\mathsf{suc}t=\mathsf{suc}u:\mathsf{N}$

$\mathrm{\Gamma }.\mathsf{N}⊢A=A^{\prime }$$\mathrm{\Gamma }⊢z=z^{\prime }:A[\mathsf{zero}]$$\mathrm{\Gamma }.\mathsf{N}.A⊢s=s^{\prime }:A[{\uparrow }^2,\mathsf{suc}{x}_1]$$\mathrm{\Gamma }⊢n=n^{\prime }:\mathsf{N}$

$\mathrm{\Gamma }⊢{\mathsf{natrec}}_{p,r}^q(A;z;s;n)={\mathsf{natrec}}_{p,r}^q(A^{\prime };z^{\prime };s^{\prime };n^{\prime }):A[n]$

$\mathrm{\Gamma }⊢A=B$$\mathrm{\Gamma }⊢t=u:\mathrm{\perp }$

$\mathrm{\Gamma }⊢{\mathsf{emptyrec}}^p(A;t)={\mathsf{emptyrec}}^p(B;u):A$

$0▸\mathsf{U}$

$0▸\mathsf{zero}$

$\gamma ▸t$$\delta ▸u$

$\gamma +\delta ▸(t,u{)}_{\otimes }$

$\gamma ▸t$$\delta ▸u$

$\gamma ▸t$

$\gamma ▸\mathsf{fst}t$

$\gamma ▸t$

$\gamma ▸\mathsf{snd}t$

$\gamma ▸t$

$\gamma ▸\mathsf{suc}t$

$\gamma ▸t$$\delta ,r,r▸u$$\eta ,q▸C$$\mathsf{Prodrec}(r)$

$r\gamma +\delta ▸{\mathsf{prodrec}}_r^q(C;t;u)$

$\gamma ▸t$$\delta ▸A$$\mathsf{Emptyrec}(p)$

$p\gamma ▸{\mathsf{emptyrec}}^p(A;t)$

$\gamma ▸t$$\delta \le \gamma$

$\delta ▸t$

$\mathrm{\Gamma }⊢t⟶u:A$$\mathrm{\Gamma }⊢A=B$

$\mathrm{\Gamma }⊢t⟶u:B$

$\mathrm{\Gamma }.A⊢B$$\mathrm{\Gamma }.A⊢t:B$$\mathrm{\Gamma }⊢u:A$

$\mathrm{\Gamma }⊢({\lambda }^{p}t){}^{p}u⟶t[u]:B[u]$

$\mathrm{\Gamma }.A⊢B$

$\mathrm{\Gamma }⊢\mathsf{fst}t⟶\mathsf{fst}{t}^{\prime }:A$

$\mathrm{\Gamma }.A⊢B$$\mathrm{\Gamma }⊢t:A$$\mathrm{\Gamma }⊢u:B[t]$

$\mathrm{\Gamma }.A⊢B$

$\mathrm{\Gamma }⊢\mathsf{snd}t⟶\mathsf{snd}{t}^{\prime }:B[\mathsf{fst}t]$

$\mathrm{\Gamma }.A⊢B$$\mathrm{\Gamma }⊢t:A$$\mathrm{\Gamma }⊢u:B[t]$

$\mathrm{\Gamma }⊢t⟶t^{\prime }:{\mathrm{\Sigma }}_{\otimes }^{q^{\prime }}AB$$\mathrm{\Gamma }.{\mathrm{\Sigma }}_{\otimes }^{q^{\prime }}AB⊢C$$\mathrm{\Gamma }.A.B⊢u:C[{\uparrow }^2,(x_1,x_0{)}_{\otimes }]$

$\mathrm{\Gamma }⊢{\mathsf{prodrec}}_r^q(C;t;u)⟶{\mathsf{prodrec}}_r^q(C;t^{\prime };u):C[t]$

$\mathrm{\Gamma }.{\mathrm{\Sigma }}_{\otimes }^{q^{\prime }}AB⊢C$$\mathrm{\Gamma }⊢t_1:A$$\mathrm{\Gamma }⊢t_2:B[t_1]$$\mathrm{\Gamma }.A.B⊢u:C[{\uparrow }^2,(x_1,x_0{)}_{\otimes }]$

$\mathrm{\Gamma }⊢{\mathsf{prodrec}}_r^q(C;(t_1,t_2{)}_{\otimes };u)⟶u[t_1,t_2]:C[(t_1,t_2{)}_{\otimes }]$

$\mathrm{\Gamma }⊢n⟶n^{\prime }:\mathsf{N}$$\mathrm{\Gamma }⊢z:A[\mathsf{zero}]$$\mathrm{\Gamma }.\mathsf{N}.A⊢s:A[{\uparrow }^2,\mathsf{suc}{x}_1]$

$\mathrm{\Gamma }⊢{\mathsf{natrec}}_{p,r}^q(A;z;s;n)⟶{\mathsf{natrec}}_{p,r}^q(A;z;s;n^{\prime }):A[n]$

$\mathrm{\Gamma }⊢z:A[\mathsf{zero}]$$\mathrm{\Gamma }.\mathsf{N}.A⊢s:A[{\uparrow }^2,\mathsf{suc}{x}_1]$

$\mathrm{\Gamma }⊢{\mathsf{natrec}}_{p,r}^q(A;z;s;\mathsf{zero})⟶z:A[\mathsf{zero}]$

$\mathrm{\Gamma }⊢z:A[\mathsf{zero}]$$\mathrm{\Gamma }.\mathsf{N}.A⊢s:A[{\uparrow }^2,\mathsf{suc}{x}_1]$$\mathrm{\Gamma }⊢n:\mathsf{N}$

$\mathrm{\Gamma }⊢{\mathsf{natrec}}_{p,r}^q(A;z;s;\mathsf{suc}n)⟶s[n,{\mathsf{natrec}}_{p,r}^q(A;z;s;n)]:A[\mathsf{suc}n]$

$\mathrm{\Gamma }⊢A$$\mathrm{\Gamma }⊢t⟶t^{\prime }:\mathrm{\perp }$

$\mathrm{\Gamma }⊢{\mathsf{emptyrec}}^p(A;t)⟶{\mathsf{emptyrec}}^p(A;t^{\prime }):A$

$(\lambda v)w⟶v[w]$

$v⟶v^{\prime }$

$vw⟶v^{\prime }w$

$v⟶v^{\prime }$

$\mathsf{fst}v⟶\mathsf{fst}{v}^{\prime }$

$\mathsf{fst}(v,w)⟶v$

$\mathsf{snd}(v,w)⟶w$

$v⟶v^{\prime }$

$\mathsf{snd}v⟶\mathsf{snd}{v}^{\prime }$

$v⟶v^{\prime }$

$\mathsf{prodrec}(v;w)⟶\mathsf{prodrec}(v^{\prime };w)$

$\mathsf{prodrec}((v,v^{\prime });w)⟶w[v,v^{\prime }]$

$\mathsf{natrec}(z;s;\mathsf{zero})⟶z$

$v⟶v^{\prime }$

$\mathsf{natrec}(z;s;v)⟶\mathsf{natrec}(z;s;v^{\prime })$

$\mathsf{natrec}(z;s;\mathsf{suc}v)⟶s[v,\mathsf{natrec}(z;s;v)]$

Dependent sessions: additional base-rule delta

The quantifier and functional-passing rules are printed in the dependent session card above. The propositions-as-sessions rules are inherited from subappendix A.61; the seven rules below are the additional base rules used by definition 102.1. Thus every omitted rule has one named earlier card rather than an implicit premise.

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

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

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

$\mathrm{\Psi };\mathrm{\Gamma };\mathrm{\Delta },x:A⟹P::z:B$

$\mathrm{\Psi };\mathrm{\Gamma };\mathrm{\Delta }⟹z(x).P::z:A⊸B$

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

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

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

$\mathrm{\Psi };\mathrm{\Gamma };\cdot ⟹!z(y).P::z:!A$

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

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

$\mathrm{\Psi };\mathrm{\Gamma };\cdot ⟹P::x:A$$\mathrm{\Psi };\mathrm{\Gamma },u:A;\mathrm{\Delta }⟹Q::z:C$

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

Dependent effects: additional operation and inclusion delta

The value/computation boundary and both bind rules are printed in the card above. The following rules supplement the point-of-use operation, stack, and machine signatures in definition 103.4, definition 103.8. Those definitions display the complete transition relation; this card does not duplicate every constructor-preserving machine frame.

$\mathrm{\Gamma },x:\mathsf{B}⊢A:\mathsf{U}$$\mathrm{\Gamma }⊢\star :A[\mathsf{true}/x]$$\mathrm{\Gamma }⊢\star :A[\mathsf{false}/x]$

$\mathrm{\Gamma },x:\mathsf{B}⊢\star :A$

$\mathrm{\Gamma }{⊢}^{\mathsf{c}}{\mathsf{diverge}}_{\underset{―}{B}}:\underset{―}{B}$

$\mathrm{\Gamma },z:U\underset{―}{B}{⊢}^{\mathsf{c}}M:\underset{―}{B}$

$\mathrm{\Gamma }{⊢}^{\mathsf{c}}{\mu }_z^{\underset{―}{B}}M:\underset{―}{B}$

$\mathrm{\Gamma }{⊢}^{\mathsf{c}}{\mathsf{error}}_{\underset{―}{B}}e:\underset{―}{B}$

$\mathrm{\Gamma }{⊢}^{\mathsf{c}}M:\underset{―}{B}$

$\mathrm{\Gamma }{⊢}^{\mathsf{c}}\mathsf{print}m.M:\underset{―}{B}$

$\{\mathrm{\Gamma }{⊢}^{\mathsf{c}}{M}_i:\underset{―}{B}{\}}_{1\le i\le n}$

$\mathrm{\Gamma }{⊢}^{\mathsf{c}}{\mathsf{choose}}_i(M_i):\underset{―}{B}$

$\mathrm{\Gamma };\underset{―}{C}{⊢}^{\mathsf{k}}\mathsf{nil}:\underset{―}{C}$

$\mathrm{\Gamma }{⊢}^{\mathsf{v}}V:A$$\mathrm{\Gamma };\underset{―}{B}[V/x]{⊢}^{\mathsf{k}}K:\underset{―}{C}$

$\mathrm{\Gamma };{\mathrm{\Pi }}_{x:A}\underset{―}{B}{⊢}^{\mathsf{k}}V::K:\underset{―}{C}$

$\mathrm{\Gamma }{⊢}^{\mathsf{c}}N:\underset{―}{B}[\mathsf{thunk}M/z]$

$\mathrm{\Gamma }{⊢}^{\mathsf{c}}N:\underset{―}{B}[\mathsf{thunk}(\mathsf{write}s.M)/z]$

$\mathrm{\Gamma }{⊢}^{\mathsf{c}}N:\underset{―}{B}[\mathsf{thunk}{M}_{s^{\prime }}/z]$

$\mathrm{\Gamma }{⊢}^{\mathsf{c}}N:\underset{―}{B}[\mathsf{thunk}({\mathsf{readto}}_s(M_s))/z]$

$\mathrm{\Gamma }{⊢}^{\mathsf{c}}N:\underset{―}{B}[\mathsf{thunk}M/z]$

$\mathrm{\Gamma }{⊢}^{\mathsf{c}}N:\underset{―}{B}[\mathsf{thunk}(\mathsf{print}m.M)/z]$

$\mathrm{\Gamma }{⊢}^{\mathsf{c}}N:\underset{―}{B}[\mathsf{thunk}{M}_{i^{\prime }}/z]$

$\mathrm{\Gamma }{⊢}^{\mathsf{c}}N:\underset{―}{B}[\mathsf{thunk}({\mathsf{choose}}_i(M_i))/z]$

Weakest preconditions: execution rules

The transformer equations and WP-Return, WP-Bind, and WP-Sub are printed in the preceding card. These are the two additional execution rules of definition 104.6.

$\mathrm{\Gamma }⊢e:\mathsf{Pure}Aw$$\mathrm{\Gamma }⊢\mathrm{\exists }p.w(p)$

$\mathrm{\Gamma }⊢\mathsf{run}e:\mathsf{Tot}A$

$\mathsf{run}(\mathsf{Pure}\mathsf{.}\mathsf{return}v)⟶v$

Dependent subtyping: additional algorithmic rule delta

The declarative product, refinement, and cast rules are printed in the card above. The following formation and bidirectional rules form the algorithmic delta of definition 106.1, definition 106.4; the complete rule families remain displayed at those definitions.

$\mathrm{\Gamma }⊢A:\mathcal{U}$$\mathrm{\Gamma },x:A⊢B:\mathcal{U}$

$\mathrm{\Gamma }⊢{\mathrm{\Pi }}_{x:A}B:\mathcal{U}$

$\mathrm{\Gamma },x:A⊢M:B$

$\mathrm{\Gamma }⊢\lambda x:A.M:{\mathrm{\Pi }}_{x:A}B$

$\mathrm{\Gamma }⊢F:{\mathrm{\Pi }}_{x:A}B$$\mathrm{\Gamma }⊢N:A$

$\mathrm{\Gamma }⊢FN:B[N/x]$

$\mathrm{fv}(\varphi )\subseteq \mathrm{dom}(\mathrm{\Gamma })\cup \{\nu \}$$\mathrm{\Gamma }⊢\mathsf{vertices}(\varphi )\mathsf{well}\text{-}\mathsf{sorted}$

$\mathrm{\Gamma }{⊢}_{\mathsf{DRef}}\{\nu :B\mid \varphi \}\mathsf{type}$

$\mathrm{\Gamma }{⊢}_{\mathsf{DRef}}R\mathsf{type}$$\mathrm{\Gamma },x:R{⊢}_{\mathsf{DRef}}S\mathsf{type}$

$\mathrm{\Gamma }{⊢}_{\mathsf{DRef}}{\mathrm{\Pi }}_{x:R}S\mathsf{type}$

$\mathrm{\Gamma }{⊢}_{\mathsf{DRef}}m\Rightarrow [m{]}_{\mathsf{Int}}$

$\mathrm{\Gamma }{⊢}_{\mathsf{DRef}}R\mathsf{type}$$\mathrm{\Gamma },x:R{⊢}_{\mathsf{DRef}}e\Rightarrow S$

$\mathrm{\Gamma }{⊢}_{\mathsf{DRef}}\lambda x:R.e\Rightarrow {\mathrm{\Pi }}_{x:R}S$

$\mathrm{\Gamma }{⊢}_{\mathsf{DRef}}e\Rightarrow {\mathrm{\Pi }}_{x:R}S$$\mathrm{\Gamma }{⊢}_{\mathsf{DRef}}v\Leftarrow R$

$\mathrm{\Gamma }{⊢}_{\mathsf{DRef}}ev\Rightarrow S[v/x]$

$\mathrm{\Gamma }{⊢}_{\mathsf{DRef}}e\Rightarrow R$

$\mathrm{\Gamma }{⊢}_{\mathsf{DRef}}e\Leftarrow S$

Dependent object types: additional structural rule delta

The selection, recursive-self, field, and tight-member rules are printed in the object-type card above. The following structural and definition rules supplement the complete point-of-use family in definition 107.2; this card does not duplicate its application, let, and evaluation-context schemas.

$\mathrm{\Gamma },x:T⊢d:T$

$\mathrm{\Gamma }⊢\nu (x:T)d:\mu (x:T)$

$\mathrm{\Gamma }⊢t:T$

$\mathrm{\Gamma }⊢\{a=t\}:\{a:T\}$

$\mathrm{\Gamma }⊢d_1:T_1$$\mathrm{\Gamma }⊢d_2:T_2$$\mathrm{dom}(d_1)\cap \mathrm{dom}(d_2)=\varnothing$

$\mathrm{\Gamma }⊢d_1\wedge d_2:T_1\wedge T_2$

Fully path-dependent types: additional replacement and lookup delta

The stable-path, singleton, replacement-leaf, and nested-initialization rules are printed in the pDOT card above. The following rules complete the named replacement descent and lookup deltas; all unchanged DOT rules are inherited from definition 107.2.

$\mathrm{\Gamma }⊢q\mathsf{path}$

$p;\mathrm{\Gamma }⊢\{a=q\}:\{a:q.\mathsf{type}\}$

$\mathrm{\Gamma }⊢\mathrm{Replace}(S,p,q,S^{\prime })$

$\mathrm{\Gamma }⊢\mathrm{Replace}(\{a:S\},p,q,\{a:S^{\prime }\})$

$\mathrm{\Gamma }⊢\mathrm{Replace}(S,p,q,S^{\prime })$

$\mathrm{\Gamma }⊢\mathrm{Replace}(\{A:S..U\},p,q,\{A:S^{\prime }..U\})$

$\mathrm{\Gamma }⊢\mathrm{Replace}(U,p,q,U^{\prime })$

$\mathrm{\Gamma }⊢\mathrm{Replace}(\{A:S..U\},p,q,\{A:S..U^{\prime }\})$

$\mathrm{\Gamma }⊢\mathrm{Replace}(S,p,q,S^{\prime })$

$\mathrm{\Gamma }⊢\mathrm{Replace}(S\wedge U,p,q,S^{\prime }\wedge U)$

$\mathrm{\Gamma }⊢\mathrm{Replace}(U,p,q,U^{\prime })$

$\mathrm{\Gamma }⊢\mathrm{Replace}(S\wedge U,p,q,S\wedge U^{\prime })$

$\mathrm{\Gamma }⊢\mathrm{Replace}(S,p,q,S^{\prime })$$\mathrm{\Gamma },x:S^{\prime }⊢U\mathsf{type}$

$\mathrm{\Gamma }⊢\mathrm{Replace}(\mathrm{\forall }(x:S)U,p,q,\mathrm{\forall }(x:S^{\prime })U)$

$\mathrm{\Gamma },x:S⊢\mathrm{Replace}(U,p,q,U^{\prime })$$x\notin \mathrm{fv}(p)\cup \mathrm{fv}(q)$

$\mathrm{\Gamma }⊢\mathrm{Replace}(\mathrm{\forall }(x:S)U,p,q,\mathrm{\forall }(x:S)U^{\prime })$

$\mathrm{\Gamma },x:\mu (x:T)⊢\mathrm{Replace}(T,p,q,T^{\prime })$$\mathrm{\Gamma }⊢\mu (x:T^{\prime })\mathsf{type}$$x\notin \mathrm{fv}(p)\cup \mathrm{fv}(q)$

$\mathrm{\Gamma }⊢\mathrm{Replace}(\mu (x:T),p,q,\mu (x:T^{\prime }))$

$\gamma (x)=v$

${\mathrm{Lookup}}_{\gamma }(x)=v$

${\mathrm{Lookup}}_{\gamma }(p)=\nu (z:T)(d_1\wedge \{a=s\}\wedge d_2)$

${\mathrm{Lookup}}_{\gamma }(p.a)=s[p/z]$

${\mathrm{Lookup}}_{\gamma }(p)=q$

${\mathrm{Lookup}}_{\gamma }(p.a)=q.a$

Proof-dependent classical control: additional dependent rule delta

The cut, control, dependent-product, NEF, and dependency-list rules are printed in the classical-control card above. The following rules form the distinctive delta of definition 109.1, definition 109.4; the ordinary positive and equality schemas remain at those point-of-use definitions.

$\mathrm{\Gamma }⊢t:\mathbb{N}$$\mathrm{\Gamma }⊢p:A[t/x]\mid \mathrm{\Delta }$

$\mathrm{\Gamma }⊢(t,p):\mathrm{\exists }x:\mathbb{N}.A\mid \mathrm{\Delta }$

$\mathrm{\Gamma }⊢p:\mathrm{\exists }x:\mathbb{N}.A\mid \mathrm{\Delta }$$p\in \mathcal{D}$

$\mathrm{\Gamma }⊢\mathrm{wit}(p):\mathbb{N}$

$\mathrm{\Gamma }⊢p:\mathrm{\exists }x:\mathbb{N}.A\mid \mathrm{\Delta }$$p\in \mathcal{D}$

$\mathrm{\Gamma }⊢\mathrm{prf}(p):A[\mathrm{wit}(p)/x]\mid \mathrm{\Delta }$

$B\in A_{\sigma }$

$\mathrm{\Gamma }\mid \widehat{\mathsf{tp}}:A{⊢}_d\mathrm{\Delta },\widehat{\mathsf{tp}}:B;\sigma \{\cdot \mid p\}$

$c:(\mathrm{\Gamma },a:A{⊢}_d\mathrm{\Delta },\widehat{\mathsf{tp}}:B;\sigma \{a\mid p\})$

$\mathrm{\Gamma }\mid \tilde{\mu }a.c:A{⊢}_d\mathrm{\Delta },\widehat{\mathsf{tp}}:B;\sigma \{\cdot \mid p\}$

$\mathrm{\Gamma }\mid {\mathrm{abort}}_{\alpha }:\mathrm{\perp }⊢\alpha :P,\mathrm{\Delta }$