A type system is, roughly, a mechanism for classifying the expressions of a language. Type systems for programming languages, sequential and concurrent, are useful for several reasons, most notably:
(1) to detect programming errors statically (2) to extract information that is useful for reasoning about the behaviour of programs (3) to improve the efficiency of code generated by a compiler (4) to make programs easier to understand.
Types are an important part of the theory and of the pragmatics of the