线性逻辑中的客户端-服务器会话
计算机科学中的逻辑
2021-03-05 v2 编程语言
摘要
我们引入共指数（coexponentials），这是经典线性逻辑的一组新模态。作为指数的对偶，共指数编码了弱化与收缩结构规则的分布式形式。这使它们成为封装服务器在单一通道上接收任意数量客户端请求的模式的合适逻辑机制。受此直觉引导，我们基于带共指数的经典线性逻辑 formulate 了一个会话类型系统，其适用于建模客户端-服务器交互。我们还提出了一种用于服务器-客户端编程的会话类型函数式编程语言，并将其翻译到我们的共指数系统。
引用
@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}
}