Typing judgment ($\Gamma ⊢e:\tau$)

A typing judgment asserts that expression $e$ has type $\tau$ under a typing context $\Gamma$. A rule displays prerequisite typing judgments above a line and their conclusion below it. Repeatedly applying rules gives a derivation; the addition example under type system uses two assumptions and one addition rule.

A typing context records the types assumed for available program names. In $\Gamma =\{x:\mathrm{int},y:\mathrm{int}\}$, looking up either name yields int. Checking a lambda abstraction extends the typing context with its argument's type for the body. In the Hindley-Milner type system, a typing context can also hold type schemes for names introduced by let polymorphism.