A type system classifies program phrases and rejects combinations that violate language-defined consistency rules before or during execution.

Formal typing is commonly written as a judgment

$$\Gamma\vdash e:T,$$

read “under typing context $\Gamma$, expression $e$ has type $T$.” The context records assumptions about free variables, for example

$$\Gamma = x:\text{Int},\ f:\text{Int}\to\text{Bool}.$$

A variable rule looks up its type in $\Gamma$. An addition rule requires both operands to be integers. A function-application rule has the form

$$\frac{\Gamma\vdash e_1:T_1\to T_2\qquad \Gamma\vdash e_2:T_1} {\Gamma\vdash e_1\ e_2:T_2}.$$

The collection of such rules is the language's static semantics: constraints checked without performing the program's ordinary runtime computation.

A type is not merely a storage size or machine representation. It is an abstraction describing which operations are permitted and what those operations produce. Different languages may make different typing judgments for similar syntax.

Writing type rules explicitly separates the language's guarantees from a particular compiler implementation and gives later proofs of type safety a precise object to reason about.