appendix sectionnotation

Effect rows and principal handler inference

symbol	meaning	first
symbol	meaning	first
$ε, μ, ⟨ ℓ ∣ ε ⟩$	finite label multiset with at most one open tail, row variable, and duplicate-preserving extension	section 25.2
$Σ$ , $P_{ℓ}$ , $R_{ℓ}$	operation signature and its parameter/response types, not a store typing	section 25.3
$σ, χ$	value scheme and type-and-effect computation scheme	section 25.2
$A! ε$	computation returning $A$ with exact effects modulo a flexible row tail	section 25.3
${gen}_{v}, {gen}_{c}$	value and computation generalization	section 25.2
$Γ ⊢_{v} v : A$ , $Γ ⊢ e : A! ε$	value and computation typing	section 25.3
$perform ℓ v$	atomic operation request	section 25.3
$handled (H)$	distinct labels with clauses in handler $H$	section 25.3
$E, R$	evaluation context and handler-free request context	section 25.3
$rewrite (ε, ℓ)$	exposure of one label occurrence with a principal substitution	section 25.4
$tail (ε)$	final row variable, when present	section 25.4
$U (A, B)$	kind-preserving type-and-row unifier	definition 25.11
$W_{v}, W_{c}$	value and computation inference	section 25.5
$X ≐ Y$ , $solve (Q; X ≐ Y)$	oriented MGU accumulator step	section 25.5
$ε \equiv ε^{'}$	duplicate-preserving row equivalence by finite permutation	definition 25.1
$M (ε)$	label-multiplicity function of an effect row	definition 25.1
$⌊ ε ⌋, ⌊ e ⌋$	closed-row support and term translation into annotated CBPV	section 25.6
$q = (m, h, w)$ , $⟨ ⟩ ⟩$ , $⟨ ℓ : q ∣ w ⟩ ⟩$	generalized evidence triple, empty vector, and newest-first extension	section 31.7
$w . ℓ$	newest-evidence selection for label $ℓ$	section 31.7
$▹$	control-monad bind in the generalized-evidence target	section 31.7
$Γ ⊢ e : σ ∣ ε ⇝ e^{'}$	type-directed GEP monadic translation	section 31.7
$λ_{∁}$ , $φ \equiv_{B} ψ$ , $φ^{c}$	Boolean equivalence in the fixed-universe exclusion calculus	section 31.8
$forb (k)$	effects forbidden by exclusion frames on stack $k$	section 31.8