appendix sectionnotation

Semantic subtyping

symbol	meaning	first
symbol	meaning	first
$0, 1$	semantic bottom and top types	chapter 9
$λ_{FG}$	finite-graph Boolean term calculus	chapter 9
$A \land B, A \lor B, \neg A$	Boolean meet, join, and complement	chapter 9
$A \leq B, A =_{D} B$	semantic inclusion and denotational equality	chapter 9
$D, D_{Ω}, Ω$	hereditary finite-graph domain, extended output domain, and failure marker	chapter 9
$Fun$	universal function-shape test $0 \to 1$	chapter 9
$F \circ S$	least application-result type	chapter 9
${proj}_{i} (P)$	least $i$ th projection-output type	chapter 9
$v ⊩ U$	runtime value $v$ passes structural test $U$	chapter 9
$vt (v)$	exact introduction type of a value	chapter 9
${syn}_{Γ} (e)$	partial annotated type synthesizer	chapter 9