线性逻辑中关于种族的探索
摘要：基于逻辑的过程演算，如πDILL和CP，为无死锁并发编程提供了基础，但排除了非确定性和竞争。HCP是对CP的改进，解决了一个根本性的缺陷：π演算中的并行组合基本操作符不对应线性逻辑的任何规则，因此也不对应CP中的任何术语构造。 我们引入了非确定性HCP，它通过新颖的非确定性机制扩展了HCP。我们的方法借鉴了有界线性逻辑，为标准的过程演算表达式提供了强类型描述的非确定性机制。我们证明了我们的扩展足够表达无类型演算中的许多非确定性使用，如非确定性选择，并保持了HCP的元理论特性，包括无死锁。
作者：Wen Kokke, J. Garrett Morris, Philip Wadler
论文ID：1909.13376
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22