Abstract

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.