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

Department of Computer Science

Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaper › Journal article › Research › peer-review

17 Citations (Scopus)

31 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
Journal	Proceedings of the ACM on Programming Languages
Volume	5
Issue	ICFP
Number of pages	31
ISSN	2475-1421
DOIs	https://doi.org/10.1145/3473567
Publication status	Published - Aug 2021

Keywords

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

Access to Document

10.1145/3473567Licence: CC BY

3473567Final published version, 437 KBLicence: CC BY

Library access?

Check availability with the Royal Danish Library

Cite this

@article{d722e32d31da4154ae64644ac0894e0f,

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 = "client-server architecture, coexponential modality, Curry-Howard, linear logic, pi-calculus, propositions as sessions, session types",

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

note = "Publisher Copyright: {\textcopyright} 2021 Owner/Author.",

year = "2021",

month = aug,

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

PY - 2021/8

Y1 - 2021/8

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 - client-server architecture

KW - coexponential modality

KW - Curry-Howard

KW - linear logic

KW - pi-calculus

KW - propositions as sessions

KW - session types

UR - https://www.scopus.com/pages/publications/85113336153

U2 - 10.1145/3473567

DO - 10.1145/3473567

M3 - Journal article

AN - SCOPUS:85113336153

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

Keywords

Access to Document

Library access?

Other files and links

Fingerprint

Cite this