Type checking checks that program statements are well-formed with respect to a typing logic [vJ11, p. 1255].

For example, integers can be added and functions can be called, but integers cannot be called and functions cannot be added.

Type checking can be used to ensure programs are type-safe, meaning that at every step of the execution, all values have well-defined and appropriate types, and that there is a valid next step of execution.