Most programming languages are equipped with a type system that detects type errors in the program, such as using a variable or result of a given type in a context that expects data of a different, incompatible type. Such type checking can take place either statically (at compile-time) or dynamically (at run-time). Type checking has proved to be very effective in catching a wide class of programming errors, from the trivial (misspelled identifiers) to the fairly deep (violations of data structure invariants). It makes program considerably safer, ensuring integrity of data structures and type-correct interconnection of program components.

Safety is not the only motivation for equipping programming languages with type systems, however. Another motivation, which came first historically, is to facilitate the efficient compilation of programs. Static typing restricts the set of programs to be compiled, possibly eliminating programs containing constructs that are difficult to compile efficiently or even to compile correctly at all. Also, static typing guarantees certain properties and invariants on the data manipulated by the program; the compiler can take advantage of these semantic guarantees to generate better code. The "Types in Compilation" workshops are dedicated to the study of these interactions between type systems and the compilation process.