3.3. Typing Judgment🔗

The judgment Γ ⊢ e : A is defined by the three usual rules: variables are typed by lookup, lambdas introduce function types, and applications eliminate function types.

\frac{x : A \in \Gamma}{\Gamma \vdash x : A} \qquad \frac{\Gamma, x : A \vdash e : B}{\Gamma \vdash \lambda x.\ e : A \to B}

\frac{\Gamma \vdash e_1 : A \to B \qquad \Gamma \vdash e_2 : A} {\Gamma \vdash e_1\ e_2 : B}

The inductive judgment below is exactly these three rules. Proofs of typing judgments are therefore derivation trees built from var, lam, and app.

The first examples are derivations of simple typing judgments. They are small enough that the proof scripts follow the inference rules directly.