Termination in Concurrency, Revisited

TL;DR

This paper compares different type systems for ensuring termination in concurrent message-passing programs, specifically within the pi-calculus, using session types as a unifying framework.

Contribution

It rigorously connects two distinct session type systems, revealing their relationship and the classes of interactions they validate for termination.

Findings

The weight-based and Curry-Howard session type systems are precisely related.

The paper clarifies which client/server interactions are considered correct by each system.

It provides a unifying perspective on termination guarantees in concurrent process typing.

Abstract

Termination is a central property in sequential programming models: a term is terminating if all its reduction sequences are finite. Termination is also important in concurrency in general, and for message-passing programs in particular. A variety of type systems that enforce termination by typing have been developed. In this paper, we rigorously compare several type systems for $\pi$-calculus processes from the unifying perspective of termination. Adopting session types as reference framework, we consider two different type systems: one follows Deng and Sangiorgi's weight-based approach; the other is Caires and Pfenning's Curry-Howard correspondence between linear logic and session types. Our technical results precisely connect these very different type systems, and shed light on the classes of client/server interactions they admit as correct.