Formal semantics and type systems describe valid reasoning using judgments and inference rules.

A judgment is a statement whose validity is defined by a formal system. Examples include

$$e\to e'$$

for one evaluation step and

$$\Gamma\vdash e:T$$

for “under assumptions $\Gamma$, expression $e$ has type $T$.”

An inference rule has premises above a line and a conclusion below it:

$$\frac{J_1\qquad J_2}{J}.$$

It says that whenever the premises $J_1$ and $J_2$ are derivable, the conclusion $J$ is derivable.

For example,

$$\frac{\Gamma\vdash e_1:\text{Int}\qquad \Gamma\vdash e_2:\text{Int}} {\Gamma\vdash e_1+e_2:\text{Int}}$$

formalizes the typing rule for integer addition.

A derivation is a tree built from inference rules whose leaves require no further justification and whose root is the judgment being proved. Rules can therefore be read both declaratively—what relations hold—and algorithmically—how a derivation may be constructed.

This notation gives programming-language definitions a precise, compositional structure and makes the cases needed in later proofs explicit.