A comparative study of type systems for deadlock-free processes
This thesis concerns verification techniques for message-passing programs, which are at the heart of the large-scale software systems that are essential to society. In this context, static verification based on type systems stands out, as it enables compositional analyses and offers rigorous correctness guarantees for programs. Many advanced type systems for message-passing concurrent programs have been developed. This raises a natural question: how do these systems relate to each other, and can they be further developed to analyze complex programs more effectively?
Logic offers a firm basis for designing type systems for concurrency. Advances leverage correspondences between linear logic (LL), the well-known logic of resources, and session types, which specify protocols for channel-based communication. These correspondences, given in the style of Curry–Howard, are often referred to as propositions-as-sessions. This thesis develops a comparative study of type systems, using propositions-as-sessions as a yardstick for comparisons, analyses, and extensions. We are interested in how logical principles enforce the deadlock freedom property, which ensures the absence of “stuck states” in interacting programs.
Our study involves various type systems for the π-calculus, each resulting from variants of LL via the Curry–Howard correspondence. We consider type systems based on intuitionistic linear logic (ILL), classical linear logic (CLL), classical linear logic with hypersequents (HLL), and differential linear logic (DiLL). We also consider a level-based type system, not based on logical principles, which enforces the (dead)lock freedom property even for process networks with circular topologies. Our goal is to relate the classes of processes induced by logic-based systems; we also aim at contrasting logical approaches with the level-based type system.
Our contributions cover different angles. We first focus on propositions-as-sessions and establish relationships between the concurrent interpretations of CLL, ILL, and HLL. We then contrast the concurrent interpretation of HLL with the level-based system, generalizing previous works. These results concern existing type systems. In the final part, we propose a new logic-based type system that extends DiLL with levels. The result is a modular type system, which uniformly combines the canonical principles of propositions-as-sessions with the effectiveness of the level-based approach. All in all, our findings reveal original insights about deadlock-freedom enforcement in message-passing concurrency; they corroborate, once again, the unusual effectiveness of logic for program analysis.