论文标题
线性逻辑中的客户端服务器会话
Client-Server Sessions in Linear Logic
论文作者
论文摘要
我们介绍了Copendentials，这是一种用于经典线性逻辑的新方式。作为指数的双重，共指数将削弱和收缩的结构规则的分布式形式编纂。这使它们成为合适的逻辑设备，用于封装从单个通道上的任意数量客户端接收请求的服务器的模式。在此直觉的指导下，我们根据经典的线性逻辑制定了一个会话类型的系统，该逻辑与copendentials一起制定，该系统适用于对客户端服务器交互进行建模。我们还提出了一种针对服务器 - 客户式编程的会话类型的功能编程语言，我们将其转换为我们的指标系统。
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.
