appendix sectionnotation

Resource and protocol notation

symbol	meaning	first
symbol	meaning	first
$V, H ⊢_{q^{'}}^{q} e ⇓ v, H^{'}$	terminating RAML evaluation with initial/residual resource	chapter 57
$Σ; Γ ⊢_{q^{'}}^{q} e : A$	typed-potential judgment with before/after constants	chapter 57
$share (A; A_{1}, A_{2})$ , $A <: B$	potential splitting and same-shape potential weakening	chapter 57
$1, \otimes, ⊸, \oplus, &$	finite logical session connectives	chapter 21
$\overset{―}{S}$	syntactic dual on the contractive tail-recursive fragment	chapter 21
$S ≃ T$	coinductively generated recursive-session equality	chapter 21
$buffered (C, Δ)$	journal graded-session channel/context invariant	chapter 21
$end$ , $G ↾ p$	terminated MPST type and partial projection to role $p$	chapter 59
$[[C {]]}_{L}$ , $[[C {]]}_{L} ↓$ , $[[C {]]}_{L} ↑$	Pirouette endpoint projection and its definedness judgments	theorem 59.8
$P \leq_{nd} Q$ , $[[R]]$	extra-local-nondeterminism preorder and result-location set	theorem 59.8

notation	meaning	owner
notation	meaning	owner
$a fresh x$ , $Γ restrict a : α \Rightarrow Γ^{'}$	nominal-set freshness and DNTT ordered-context restriction	chapter 64
$N a : α . B$ , $⟨ a : α ⟩ M$ , $M @ a$	dependent name abstraction, introduction, and concretion	chapter 64
$Γ ⊢ p$ , $(@)_{α}$ , $thm$	HOL sequents, polymorphic choice, and the host-level abstract theorem type	chapter 24
$R_{σ}$ , $R_{σ}$	System T primitive recursion and reducibility at finite type $σ$	chapter 66
$A^{D} = \exists \vec{x} \forall \vec{y} . A_{D} (\vec{x}, \vec{y})$	Dialectica interpretation and its quantifier-free matrix	chapter 66