2023/08/02 by Joseph W. N. Paulus, Paulus, Joseph W. N., Jorge A. Pérez +3
Computer Science · #Distributed systems and fault tolerance #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.2308.01165
openalex publication_date 2023/08/02 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.