优先选择最佳变体
摘要：二进制会话类型保证通信的安全性和会话的忠诚度，但是单独的它们无法排除来自不同会话交错的死锁。在经典进程（CP）中，基于经典线性逻辑的进程演算中，通过将通道创建和并行组合在同一逻辑割规则下来保证无死锁。类似地，在Good Variation（GV）中，一个线性并发λ-演算，通过将通道创建和线程生成组合在同一操作中（称为fork）来保证无死锁。在CP和GV中，通过牺牲表达性来实现无死锁，因为只允许树结构的进程。Dardha和Gay定义了Priority CP（PCP），允许循环结构的进程，并通过使用优先级来恢复无死锁，与Kobayashi和Padovani保持一致。在PCP之后，我们提出了Priority GV（PGV），GV的一个变体，分离了通道创建和线程生成。因此，我们可以为循环结构的进程提供类型，并通过使用优先级来恢复无死锁。我们通过证明主题规约和进展来证明我们的类型系统的正确性。我们定义了从PCP到PGV的编码，并证明编码保持类型，并且相对于操作语义是正确完备的。
作者：Wen Kokke and Ornela Dardha
论文ID：2103.14466
分类：Programming Languages
分类简称：cs.PL
提交时间：2022-12-26