Type checking is a program analysis that verifies something about the types that are used in the program.

In the strictest sense, the sense found in programming language analysis conferences, the analysis verifies (when it is successful) that the analyzed program will not have type errors when it executes (i.e. it will be TypeSafe).

In a weaker but more common sense, type checking doesn't verify anything in particular, although it may provide some amount of TypeSafety. The stronger sense applies to MlLanguage, while the weaker sense applies to CeeLanguage.

See StronglyTyped and StronglyTypedWithoutLoopholes.
----
CategoryLanguageTyping