Client-Server Sessions in Linear Logic

Zesen Qian*, G. A. Kavvos*, Lars Birkedal*

*Corresponding author for this work

Research output: Contribution to journalArticle (Academic Journal)peer-review

1 Citation (Scopus)
7 Downloads (Pure)

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 languageEnglish
Article number62
Number of pages32
JournalProceedings of the ACM on Programming Languages
Volume5
Issue numberICFP
DOIs
Publication statusPublished - 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

Fingerprint

Dive into the research topics of 'Client-Server Sessions in Linear Logic'. Together they form a unique fingerprint.

Cite this