appendix sectionnotation

System F

symbol	meaning	first
symbol	meaning	first
$Δ; Γ ⊢ t : A$	Church-style System F typing	5
$Δ; Γ ⊢_{C} m : A$	Curry-style System F typing	5
$Λ X . t, t [A]$	type abstraction and type application	5
$t ⟶_{β} t^{'}$	one compatible term-beta step, including type-beta roots	5
$t ⟶_{β}^{*} t^{'}$	reflexive–transitive compatible term-beta reduction	5
$t ⇛_{β} t^{'}$	one parallel beta step on System F terms	9.40
$t ⇛_{β}^{*} t^{'}$	reflexive–transitive parallel beta reduction	5.38
$t \Leftarrow_{β}^{*} t^{'}$	reverse reflexive–transitive parallel beta reduction	5.38
$SN$	strongly normalizing terms	5
$[[A {]]}_{η}$	reducibility-candidate interpretation	5