appendix sectionnotation

Capture, typestate, and coeffect notation

symbol	meaning	first
symbol	meaning	first
$C ▹ U$	pretype $U$ with indirect capture upper bound $C$	section 51.1
$C_{1} ≼_{cap} C_{2}$	indirect subcapturing preorder in ${CF}_{<:}$	section 51.2
$t ⟶_{cap} t^{'}$	one call-by-value ${CF}_{<:}$ step	section 51.4
$t ⟶_{cap}^{*} t^{'}$	reflexive-transitive ${CF}_{<:}$ reduction	theorem 51.8
$Σ {ok}_{◻} V$	state typing in the separate boxed capture calculus	subsection 51.5.1
$Σ ⟶_{◻} Σ^{'}$	one machine step in the separate boxed capture calculus	subsection 51.5.1
$H, η ⊧_{ts} Δ$	runtime heap and value environment agree with a protocol context	definition 52.1
$c ⟶_{ts} c^{'}$	one affine file-protocol configuration step	section 52.3
$c ⟶_{ts}^{*} c^{'}$	reflexive-transitive affine file-protocol reduction	section 52.3
$File [q] ⊸ Δ$	checked typestate procedure from one handle to an output context	section 52.2
$r ⊛ s$ , $r \oplus_{c} s$	sequential and sharing composition of coeffect scalars	section 53.1
$r \land_{c} s$	flat abstraction combination, constrained by condition $F$	section 53.1
$Γ @_{f} r ⊢ e : τ$	flat whole-context coeffect judgment	section 53.1
$Γ @_{s} R ⊢ e : τ$	structural per-variable coeffect judgment	section 53.4
$Γ^{'} @_{s} R^{'} ⇝_{ctx, θ} Γ @_{s} R$	structural coeffect context transformation	section 53.4
$σ {\overset{r}{\to}}_{c} τ$	function type with latent coeffect scalar $r$	section 53.1
$ρ ⊧_{d} R$	typed dictionary $ρ$ realizes requirement set $R$	section 53.5
$c ⟶_{df} v$	one dedicated causal-dataflow history lookup	section 53.5