Typing environment
In type theory, a typing environment represents the association between variable names and data types.
More formally, an environment is a set or ordered list of pairs, usually written as, where is a variable and its type.
The judgement
is read as " has type in context ".
For each function body type checks:
Typing Rules Example:
In statically typed programming languages, these environments are used and maintained by typing rules to type check a given program or expression.