会话类型中域的子指数视角
计算机科学中的逻辑
2022-04-11 v2
摘要
线性逻辑（LL）启发了许多计算系统的设计，提供了构建于其元理论之上的推理技术。自其诞生以来，从不同的视角涌现了并发系统与 LL 之间的若干联系。在过去十年中，Caires 和 Pfenning 的开创性工作表明，LL 中的公式可解释为会话类型，而 pi-演算中的进程可作为证明项。这导致了一种 Curry-Howard 解释，其中消去切割过程中的证明归约对应于进程归约/交互。LL 中的子指数在并发系统中也发挥了重要作用，因为它们可以以不同方式解释，包括分布式系统中的时间、空间乃至认知模态。在本文中，我们探讨如下问题：从会话类型解释的角度看，子指数的含义是什么？我们的回答是一个类 pi 的进程演算，其中智能体驻留在位置/站点中，并显式地指明不同站点之间的通信应如何发生。该语言的设计完全依赖于 LL 中子指数的证明理论，从而以优雅的方式扩展了 Caires-Pfenning 解释。
引用
@article{arxiv.2110.03964,
title = {A Subexponential View of Domains in Session Types},
author = {Daniele Nantes and Carlos Olarte and Daniel Ventura},
journal= {arXiv preprint arXiv:2110.03964},
year = {2022}
}
备注
In Proceedings LSFA 2021, arXiv:2204.03415