Types and Programming Languages

⇒ arrow kind, 441

⇓ big-step evaluation, 42

Π dependent function type, 463

:: derivation of, 203

↑ divergence, 16

dom(Г) domain of Г, 101

⋆ "quick check" exercise, xviii

⋆⋆ easy exercise, xviii

⋆⋆⋆ moderate exercise, xviii

⋆⋆⋆⋆ challenging exercise, xviii

↛ exercise without solution, xviii

→ function type, 100

:: kind membership, 449

→* multi-step evaluation, 39

→ one-step evaluation, 36

⇛ parallel reduction of types, 454

L record labels, 129

R⁺ transitive closure of R, 17

R* reflexive, transitive closure, 17

▸ sample output from system, 25

\ set difference, 15

↑^d() shifting, 79

σ ∘ γ substitution composition, 318

<: subtyping, 181

↓ termination, 16

≡ type equivalence, 447, 453

: type membership, 92

_ wildcard binder, 46, 121

α conversion, 71