一句话：将非确定性引入基于线性逻辑的 HCP 进程演算，在保持无死锁性的同时刻画竞态与选择。
基于逻辑的进程演算（如 πDILL、CP）为无死锁并发编程提供了基础，但排除了非确定性与竞态；HCP 虽改进 CP 中并行组合无法对应线性逻辑规则的问题，仍缺乏对非确定性的处理。本文提出非确定性 HCP，借助有界线性逻辑为传统进程演算中的非确定性表达式给出强类型刻画，将非确定性选择等构造纳入 HCP。作者证明该扩展足以表达无类型演算中的多种非确定性用法，同时保持 HCP 的元理论性质，包括无死锁性。
Process calculi based in logic, such as $\pi$DILL and CP, provide a foundation for deadlock-free concurrent programming, but exclude non-determinism and races. HCP is a reformulation of CP which addresses a fundamental shortcoming: the fundamental operator for parallel composition from the $\pi$-calculus does not correspond to any rule of linear logic, and therefore not to any term construct in CP. We introduce non-deterministic HCP, which extends HCP with a novel account of non-determinism. Our approach draws on bounded linear logic to provide a strongly-typed account of standard process calculus expressions of non-determinism. We show that our extension is expressive enough to capture many uses of non-determinism in untyped calculi, such as non-deterministic choice, while preserving HCP's meta-theoretic properties, including deadlock freedom.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{KokkeMW20,
title = {Towards Races in Linear Logic},
author = {Wen Kokke and J. Garrett Morris and Philip Wadler},
journal = {Logical Methods in Computer Science},
volume = {Volume 16, Issue 4},
year = {2020},
doi = {10.23638/lmcs-16(4:15)2020}
}