appendix sectionnotation

Graded-base, temporal, and soft-logic notation

symbol	meaning	first
symbol	meaning	first
$r ⊑_{q} s$	approximation preorder on grades	section 54.1
$t ⟶_{L} t^{'}$ , $t ⟶_{L}^{*} t^{'}$	Linear Base one-step relation and its closure	section 54.2, section 54.3
$t ⟶_{G} t^{'}$ , $t ⟶_{G}^{*} t^{'}$	Graded Base one-step relation and its closure	section 54.3
$L [[t]]$ , $G [[t]]$	direct graded-to-linear and CPS linear-to-graded translations	section 54.4, section 54.5
$T_{e} A$ , $D_{r} A$ , $x : [A]_{r}$ , $A < :_{ec} B$	combined-calculus effect type, coeffect type, discharged assumption, and subtyping relation	section 54.6
$H ⊢ t ⇝_{fu} H^{'} ⊢ t^{'}$ , $H ⋈_{h} Γ$	fractional machine step and heap/context compatibility	section 54.7
$◯ A$ , $◻ A$	Simply RaTT later and stable modalities	section 55.2
$Ev A ≅_{ev} A + ◯ (Ev A)$	guarded recursive event isomorphism	section 55.3
$▸$ , $✓$	Simply RaTT Fitch lock and tick	section 55.2
$⟹_{s}$ , $⟹_{t}^{v / v^{'}}$	stream step and input/output transducer step	section 55.4
$V [[A]]$ , $T [[A]]$ , $C [[Γ]]$	Simply RaTT value, term, and context logical relations	section 55.5
$w ⪯_{w} w^{'}$	extension of a Simply RaTT logical-relation world	section 55.5
$Clock$ , $Flow A$	Boolean stream and stream of optional $A$ -values	section 55.3
$[τ] X$ , $X! τ$ , $⟨ τ ⟩$ , $s ⟼_{tr} s^{'}$	temporal-resource value type, computation type, and elapsed-time context marker, with its machine step	section 55.6
$u ⟶_{SLL} v$ , $u ⟶_{SLL}^{*} v$	one external SLL proof-net reduction and its closure	section 56.2
$W_{u} (X)$	Lafont proof-net weight polynomial	section 56.2
$S^{(m)}$	$m$ separate string assumptions, not iterated boxes	section 56.3