sMALL CaPS: An Infinitary Linear Logic for a Calculus of Pure Sessions

We present an infinitary version of Multiplicative Additive Linear Logic (sMALL) that serves as logical foundation for a Calculus of Pure Sessions (CaPS). sMALL is infinitary not only because proof derivations may be infinite, but also because propositions themselves may be infinite. In this sense, sMALL differs from other related extensions of Linear Logic based on least and greatest fixed points. Also, all sMALL derivations are valid proofs by construction. sMALL enables the description and implementation in CaPS of recursive communication protocols – like authentication, coordination, consensus – in which termination is not decided autonomously by a single process, but results from some negotiation involving two or more interacting processes. We prove that sMALL is sound and that it enjoys cut elimination. We also prove a relative completeness result showing that a certain class of well-behaving CaPS processes are well typed in sMALL. Finally, we show that sMALL can be easily extended to address a broader class of fairly terminating processes, those that terminate under a suitable fairness assumption.