typing environment

In type theory, a typing environment (or typing context) represents the association between variable names and data types.

More formally, an environment $\Gamma$ is a set or ordered list of pairs $\langle x,\tau \rangle$, usually written as $x:\tau$, where $x$ is a variable and $\tau$ its type.

The judgement
: $\Gamma \vdash e:\tau$
is read as "$e$ has type $\tau$ in context $\Gamma$ ".

For each function body type checks:
:$\Gamma = \$

Typing Rules Example:
$\begin \Gamma\vdash b:Bool, \Gamma\vdash t_1:\tau, \Gamma\vdash t_2:\tau\\ \hline \Gamma \vdash (\text(b) t_1 \text t_2): \tau \\ \end$

In statically typed programming languages, these environments are used and maintained by typing rules to type check a given program or expression.

See also

* Type system

References

Data types
Program analysis
Type theory

{{type-theory-stub