Typing judgment

A formal statement asserting that a term has a particular type under a given Type environment, typically written as $\Gamma \vdash t : T$.