Client-Server Sessions in Linear Logic
Logic in Computer Science
2021-03-05 v2 Programming Languages
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 server-client programming, which we translate to our system of coexponentials.
Cite
@article{arxiv.2010.13926,
title = {Client-Server Sessions in Linear Logic},
author = {Zesen Qian and G. A. Kavvos and Lars Birkedal},
journal= {arXiv preprint arXiv:2010.13926},
year = {2021}
}