Static Type System

type-theory

Definition

Static Type System

A static type system is a type system whose typing judgements are checked before program execution.

Formally, for an expression $e$, type environment $\Gamma$, and type $\tau$, the system accepts only when it can derive

$$\Gamma ⊢e:\tau$$

without evaluating $e$.