Type-based deadlock analysis of linear communications

In this seminar we will study a typing discipline that ensures the absence of deadlocks in systems of processes that communicate on linear channels (channels that can be used for one communication only). This seemingly simple communication model, together with the possibility of sending channels as messages, suffices to capture a range of actual systems, including parallel algorithms, binary and multiparty sessions, and data-flow networks. We will introduce the type system using an abstract process language (the pi calculus) and then we will see how to adapt the type system so that it applies to a more concrete programming language with higher-order functions.