Typing Judgement

type-theory

Definition

Typing Judgement

A typing judgement is a formal assertion that an expression has a type under a given type environment.

Its standard form is

$$\Gamma ⊢e:\tau ,$$

where $\Gamma$ is a type environment, $e$ is an expression, and $\tau$ is a type.