Session types are designed to abstractly capture the structure of (even multi-party) communication protocols. The goal of session types is the analysis and verification of the protocols’ behavioural properties. One important such property is progress, i.e., the absence of (unintended) deadlock. Distributed algorithms often resemble (compositions of) multi-party communication protocols. In contrast to protocols that are typically studied with session types, they are often designed to cope with faults, like system failures. An essential behavioural property is (successful) fault-tolerant termination, but it is often elaborate to prove for distributed algorithms.

The talk is about an extension of multi-party session types to capture faults due to message loss and process crashes. It combines reliable and unreliable communication mechanisms in types and augment the semantics of processes by failure patterns that can be used to represent system requirements (as, e.g., failure detectors).