Termination in Concurrency, Revisited
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 -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.
Cite
@article{arxiv.2308.01165,
title = {Termination in Concurrency, Revisited},
author = {Joseph W. N. Paulus and Jorge A. Pérez and Daniele Nantes-Sobrinho},
journal= {arXiv preprint arXiv:2308.01165},
year = {2023}
}