Client-Server Sessions in Linear Logic

Zesen Qian; G. A. Kavvos; Lars Birkedal

doi:10.1145/3473567

Client-Server Sessions in Linear Logic

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

^*Corresponding author for this work

Research output: Contribution to journal › Article (Academic Journal) › peer-review

17 Citations (Scopus)

316 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 language	English
Article number	62
Number of pages	32
Journal	Proceedings of the ACM on Programming Languages
Volume	5
Issue number	ICFP
DOIs	https://doi.org/10.1145/3473567
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.

Research Groups and Themes

Programming Languages

Keywords

session types
linear logic
propositions as sessions
Curry-Howard
𝜋-calculus
coexponential modality
client-server architecture

Access to Document

10.1145/3473567

Full-text PDF (final published version)
This is the final published version of the article (version of record). It first appeared online via Association for Computing Machinery at https://doi.org/10.1145/3473567 . Please refer to any applicable terms of use of the publisher.
Final published version, 439 KBLicence: CC BY

Handle.net

Persistent link

ICFP Distinguished Paper Award
Qian, Z. (Recipient), Kavvos, A. (Recipient) & Birkedal, L. (Recipient), 13 Sept 2021
Prize: Prizes, Medals, Awards and Grants

Cite this

@article{8657a83e507c4ccfb39ba0b2ff29b7d3,

title = "Client-Server Sessions in Linear Logic",

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.",

keywords = "session types, linear logic, propositions as sessions, Curry-Howard, 𝜋-calculus, coexponential modality, client-server architecture",

author = "Zesen Qian and Kavvos, \{G. A.\} and Lars Birkedal",

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: {\textcopyright} 2021 Owner/Author.",

year = "2021",

month = aug,

day = "18",

doi = "10.1145/3473567",

language = "English",

volume = "5",

journal = "Proceedings of the ACM on Programming Languages",

issn = "2475-1421",

publisher = "Association for Computing Machinery",

number = "ICFP",

}

TY - JOUR

T1 - Client-Server Sessions in Linear Logic

AU - Qian, Zesen

AU - Kavvos, G. A.

AU - Birkedal, Lars

N1 - 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.

PY - 2021/8/18

Y1 - 2021/8/18

N2 - 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.

AB - 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.

KW - session types

KW - linear logic

KW - propositions as sessions

KW - Curry-Howard

KW - 𝜋-calculus

KW - coexponential modality

KW - client-server architecture

U2 - 10.1145/3473567

DO - 10.1145/3473567

M3 - Article (Academic Journal)

SN - 2475-1421

VL - 5

JO - Proceedings of the ACM on Programming Languages

JF - Proceedings of the ACM on Programming Languages

IS - ICFP

M1 - 62

ER -

Client-Server Sessions in Linear Logic

Abstract

Bibliographical note

Research Groups and Themes

Keywords

Access to Document

Handle.net

Fingerprint

Prizes

ICFP Distinguished Paper Award

Cite this