A type checking algorithm for qualified session types

TL;DR

This paper introduces a type checking algorithm for session types in the pi calculus, distinguishing linear and unrestricted channels to ensure safe communication protocols and resource usage.

Contribution

It proposes a novel type checking algorithm for qualified session types in the pi calculus, ensuring soundness and consistency in resource management.

Findings

The algorithm guarantees linear channels are used exactly once before becoming unrestricted.

Type checking preserves typings during process computation.

The approach ensures soundness and structural congruence consistency.

Abstract

We present a type checking algorithm for establishing a session-based discipline in the pi calculus of Milner, Parrow and Walker. Our session types are qualified as linear or unrestricted. Linearly typed communication channels are guaranteed to occur in exactly one thread, possibly multiple times; afterwards they evolve as unrestricted channels. Session protocols are described by a type constructor that denotes the two ends of one and the same communication channel. We ensure the soundness of the algorithm by showing that processes consuming all linear resources are accepted by a type system preserving typings during the computation and that type checking is consistent w.r.t. structural congruence.