appendix sectionnotation

Regions and capabilities

symbol	meaning	first
symbol	meaning	first
$get (ρ), put (ρ)$	region read and allocation/write effects	chapter 50
$TE ⊢ e ⇝ e^{'} : μ, ϕ$	Tofte–Talpin region-annotation judgment	section 50.1
$C (R, TE, E, s, V E)$	Tofte–Talpin inference/execution consistency relation	theorem 50.2
$ϵ$	Tofte–Talpin effect handle in section 50.1; Cyclone live-region set in section 50.5	chapter 50
${r^{+}}, {r^{1}}$	duplicable and unique region authority	section 50.3
$C_{1} \oplus C_{2}$	capability combination, not numeric addition	section 50.3
$\overset{―}{C}$	stripping of unique capability flags	section 50.3
$C_{1} =_{Cap} C_{2}, C_{1} \leq_{Cap} C_{2}$	capability equality and inclusion under $Δ$	section 50.3
$Ψ ⊧ C$	memory type satisfies exactly the live-region capability	definition 50.3
$⟶$	one capability-machine transition	section 50.3
$CapOf (ψ)$	syntactic translation of a region effect to a capability	section 50.4
$r_{1} ⪰ r_{2}$	Cyclone lifetime ordering, longer region first	section 50.5
$⟶_{L^{3}}, ⟶_{lr}, ⟶_{lr}^{*}$	L3 single step; linear-region single and multi-step reduction	definition 50.11
$⟼_{FRGN}, ≫ =_{FRGN}$	FRGN interface-state step and monadic bind	definition 50.13