Type systems for programming languages help reasoning about program
behavior and early finding of bugs. Recent applications of type systems
include analysis of various program behaviors such as side
effects, resource usage, security properties, and concurrency.
This paper is a tutorial of one of such applications:
type systems for analyzing behavior of concurrent processes.
We start with a simple type system and extend it step by
step to obtain more expressive type systems to reason about
deadlock-freedom, safe usage of locks, etc.