appendix sectionnotation

Interaction trees, modules, and possibilities

notation	meaning	owner
notation	meaning	owner
$ITree (E, R)$ , $Ret$ , $Vis$ , $Tau$	guarded interaction trees and their three observations	chapter 86
$sbisim (t, u)$ , $eutt (t, u)$	strong bisimulation and termination-sensitive weak equivalence	chapter 86
$interp (H, t)$ , $E +_{E} F$	handler interpretation and tagged event-signature sum	chapter 86
${Spec}_{T} (E)$ , $Impl (E, F)$	finite-thread LTS specification and module implementation	chapter 87
$V ▹ M$ , $V_{1} ≅ V_{2}$ , $V_{1} \otimes V_{2}$	vertical linking, linked-LTS isomorphism, and tagged horizontal tensor	chapter 87
$K (V)$ , $Ref (V^{'}, V)$ , $Lin (V^{'}, V)$	identity saturation, trace refinement, and compositional linearizability	chapter 87
$ρ = ⟨ ρ_{S}, ρ_{C}, ρ_{R} ⟩$ , $PossSet (V)$	target possibility and predicate-represented possibility set	chapter 88
${Commit}_{i}$ , ${Silent}_{i}$ , ${ReturnStep}_{i}$ , ${ConsumeSet}_{i, m, v}$ , $VerifyImpl$	visible commit, silent obligation, overlay-return consumption, and verified module record	chapter 88