Type-Based Analysis for Session Inference

TL;DR

This paper introduces a type-based analysis method for inferring session protocols in a concurrent functional language, ensuring communication safety and lock freedom without linearity, and enabling complete session inference.

Contribution

It develops a novel type-checking system that separates ML types from session types, supporting inference without annotations and handling cases beyond substructural type systems.

Findings

Guarantees communication safety and partial lock freedom

Supports provably complete session inference for finite sessions

Handles examples not typable in substructural type systems

Abstract

We propose a type-based analysis to infer the session protocols of channels in an ML-like concurrent functional language. Combining and extending well-known techniques, we develop a type-checking system that separates the underlying ML type system from the typing of sessions. Without using linearity, our system guarantees communication safety and partial lock freedom. It also supports provably complete session inference for finite sessions with no programmer annotations. We exhibit the usefulness of our system with interesting examples, including one which is not typable in substructural type systems.