Definition
Type System
A type system is a formal system that assigns types to expressions and rejects expressions whose assigned types violate its typing rules.
Formally, it defines a derivability relation
where is a type environment, is an expression, and is a type.