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