appendix sectionnotation

Self types, F-bounds, and matching

symbol	meaning	first
symbol	meaning	first
$Δ; Γ$ , $Ξ$ , $Σ$	type/term contexts, matching context, and store typing	definition 16.4, definition 16.13
$Self ρ . R (ρ)$	covariant package hiding representation $ρ$ , not an effect row	definition 16.4
$packSelf C with v as S$ , $useSelf t as X, x in u$	Self introduction and elimination	definition 16.4
$F_{eq}$ , $⪯^{+}$ , $⪯^{-}$	equi-recursive comparison and positive/negative simulation	definition 16.11
$\forall X <: F (X) . A$	F-bounded quantification	definition 16.11
$A # B$ , $Ξ$	protocol matching and its assumption context; no value subsumption	definition 16.13
$Oper (A)$ , $A^{†}$ , $Ξ^{†}$	source protocol operator and matching-to-operator syntax translations	definition 16.13
$Φ_{X} ⪯ F$	target operator-bound assumption	definition 21.13
$preMax$	source match-polymorphic binary client	definition 16.13
$W^{'} ⪰ W$ , $σ ⊧_{n} W$	world extension and indexed heap satisfaction	definition 21.20
$V [[A {]]}_{θ} (W, n)$ , $E [[A {]]}_{θ} (W, n)$	semantic value and expression interpretations	definition 21.20