Abstract
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.
| Original language | English |
|---|---|
| Article number | 62 |
| Number of pages | 32 |
| Journal | Proceedings of the ACM on Programming Languages |
| Volume | 5 |
| Issue number | ICFP |
| DOIs | |
| Publication status | Published - 18 Aug 2021 |
Bibliographical note
Funding 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.
Publisher Copyright:
© 2021 Owner/Author.
Structured keywords
- Programming Languages
Keywords
- session types
- linear logic
- propositions as sessions
- Curry-Howard
- 𝜋-calculus
- coexponential modality
- client-server architecture