We introduce coexponentials, a new set of modalities for Classical Linear Logic. As duals to exponentials, the coexponentials codify a distributed form of the structural rules of weakening and contraction. This makes them a suitable logical device for encapsulating the pattern of a server receiving requests from an arbitrary number of clients on a single channel. Guided by this intuition we formulate a system of session types based on Classical Linear Logic with coexponentials, which is suited to modelling client-server interactions. We also present a session-typed functional programming language for client-server programming, which we translate to our system of coexponentials.
Bibliographical noteFunding Information:
Alex Kavvos was supported in part by a research grant (no. 12386, Guarded Homotopy Type Theory) from the VILLUM Foundation. This work was also supported in part by a Villum Investigator grant (no. 25804, Center for Basic Research in Program Verification (CPV)). We gratefully acknowledge discussions with Martin Berger, Amar Hadzihasanovic, Vladimir Zamdzhiev, Wen Kokke, Fabrizio Montesi and Marco Peressotti.
Won the Distinguished Paper Award at ICFP 2021.
© 2021 Owner/Author.
- Programming Languages
- session types
- linear logic
- propositions as sessions
- coexponential modality
- client-server architecture