appendix sectionnotation

Effects, CBPV, and algebraic handlers

symbol	meaning	first
symbol	meaning	first
$Σ (op) = P_{op} ⇝ R_{op}$	operation signature, not a store typing	chapter 22
$T_{Σ} A$ , $Ret$ , ${Op}_{op}$	well-founded free operation trees and constructors	22.1
$return$ , $≫ =$	tree return and sequencing	22.2
${fold}_{r, h}$	unique handler-algebra fold	22.7
$Γ ⊢_{v} V : A$ , $Γ ⊢_{c} M : C$	CBPV value and computation typing	22.10
$U C$ , $F A$ , $A \Rightarrow C$	thunk, returned-value, and value-to-computation types	22.10
$e^{v}$ , $w_{v}^{†}$ , $e^{n}$	call-by-value computation/value and call-by-name syntax translations	22.5
$⇝_{a}$ , $\equiv_{a}$ , $M^{a}$	administrative force–thunk contraction, congruence, and normal form	22.16
$ℓ (M)$ , $ℓ_{a} (M)$	weak-trace length and administration-invariant cost	22.18
$C! E$	computation exposing at most the finite operation set $E$	22.20
$U_{E} C$ , $A \Rightarrow^{E} C$	thunk-latent and arrow-latent operations	22.20
$handled (H)$	operation names with clauses in $H$	22.20
$Γ ⊢_{h} H$	handler typing from $A [E]$ to $B [D]$	22.20
$X_{op}$ , $\hat{k}$	operation-open evaluation context and reinstalled deep continuation	22.7
$X_{op}^{fo}$	application-free operation-open context for first-order reification	22.9
$[[L {]]}_{ρ, κ}$	semantic first-order tree reification; $ρ$ is a value environment	22.9