Detail

Type-Based Analysis for Session Inference

A binary session type describes the sequence and types of messages that two concurrent processes exchange over a particular channel. Thanks to this formalism, several useful properties of concurrent programs can be verified at compilation time, such as the safe exchange of messages. The burden of extracting session types from the source code is often shared with the programmer, who might have to refactor the code or manually decorate it with type annotations.

In this talk I propose a framework that:

1) infers session types without programmer annotations for an ML-like concurrent functional language, and 2) provides useful guarantees such as deadlock-freedom (up to specific conditions).

The framework combines and extends well-known static analysis techniques called type-based analysis, that leverage the fact that a program is well-typed. The usefulness of the system is discussed by examples.