Typing environment

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

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

The judgement

${\displaystyle \Gamma \vdash e:\tau }$

is read as "${\displaystyle e}$ has type ${\displaystyle \tau }$ in context ${\displaystyle \Gamma }$ ".^[1]

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

See also[]

• Type system

References[]

${\displaystyle \Gamma \vdash x:{\text{Int}}}$

This programming language theory or type theory-related article is a stub. You can help Wikipedia by .

• v
• t