Typing environment

In type theory a typing environment (or typing context) represents the association between variable names and data types.
More formally an environment formula_1 is a set or ordered list of pairs formula_2, usually written as formula_3, where formula_4 is a variable and formula_5 its type.
The judgement
is read as "formula_7 has type formula_5 in context formula_1 ".
In statically typed programming languages these environments are used and maintained by type rules to type check a given program or expression.