appendix sectionnotation

Difference refinements and certificates

symbol	meaning	first
symbol	meaning	first
$L_{a}$	logical measure $len (a)$	chapter 10
$r - s \leq k$	integer difference atom	chapter 10
$\overset{―}{δ}$	integer complement of $δ$	chapter 10
${ν : B ∣ p}$	base refinement type	chapter 10
$x : s \to t$	refinement arrow with restricted result dependency	chapter 10
$V (Γ)$	logical vertices available from $Γ$	chapter 10
$⌊ Γ ⌋$	conjunction embedded by a refinement context	chapter 10
$Γ ⊧_{all} p$	semantic entailment in difference logic	chapter 10
$ρ ⊧ Γ$	valuation satisfaction for a refinement context	chapter 10
$G_{Γ}$	identified-edge constraint graph	chapter 10
$e_{1} ▹_{x} e_{2}$	A-normal bind composition	chapter 10
$Γ ⊢ a \Rightarrow t$	refinement atom synthesis	chapter 10
$Γ ⊢ c \Rightarrow_{c} t$	refinement computation synthesis	chapter 10
$Γ ⊢ e \Leftarrow t$	refinement expression checking	chapter 10
$SubVC (Γ; s, t)$	partial subtyping-to-VC translation	chapter 10
$A_{Γ}, {Comp}_{Γ}, K_{Γ}$	atom synthesis, computation synthesis, and expression checking functions	chapter 10
$Bnd (a, i)$	conjunction $0 \leq i < len (a)$	chapter 10
$guard (p, e)$	nested first-order dynamic check	chapter 10
$loop$	named divergent recursive program used in the conservativeness example	chapter 10
$\| t \|, \| e \|$	refinement type shape and term erasure	chapter 10