基于线性逻辑的类型会话系统：经典与直觉主义的比较
计算机科学中的逻辑
2020-04-06 v1 编程语言
摘要
会话类型系统已通过基于直觉主义与经典线性逻辑的 Curry-Howard 对应获得了逻辑基础。由两种逻辑导出的类型系统在同一类 pi 演算进程上强制通信正确性，但它们有显著差异。Caires、Pfenning 和 Toninho 非正式地观察到，与经典类型系统不同，直觉主义类型系统对共享通道强制局部性，即接收到的通道不能用于复制输入。本文从形式化角度重新审视该观察。我们开发了统一线性逻辑（ULL），一种涵盖经典与直觉主义线性逻辑的逻辑。随后，遵循会话类型的 Curry-Howard 对应，我们定义了 piULL，一种基于 ULL 的 pi 演算会话类型系统。利用 piULL，我们可以形式化评估直觉主义与经典类型系统之间的差异，并论证局部性与对称性在其中所起的作用。
引用
@article{arxiv.2004.01320,
title = {Session Type Systems based on Linear Logic: Classical versus Intuitionistic},
author = {Bas van den Heuvel and Jorge A. Pérez},
journal= {arXiv preprint arXiv:2004.01320},
year = {2020}
}
备注
In Proceedings PLACES 2020, arXiv:2004.01062