Client-Server Sessions in Linear Logic

TL;DR

This paper introduces coexponentials in Classical Linear Logic to model distributed client-server interactions, and develops a session-typed programming language based on this logic for server-client programming.

Contribution

It presents the novel concept of coexponentials as duals to exponentials, enabling logical modeling of client-server communication patterns.

Findings

Coexponentials effectively model distributed server requests.

A session-typed language based on coexponentials is developed.

The system accurately captures client-server interaction protocols.

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.