确保线性 π-演算中公平终止的线性逻辑无穷证明论
计算机科学中的逻辑
2022-07-11 v1 编程语言
摘要
公平终止是程序的一种性质：程序“原则上”可能发散，但在“实际中”会终止，即在关于非确定性选择解决的合适公平性假设下终止。我们研究 MALL 的一个保守扩展，它是具有最小和最大不动点的线性逻辑乘法加法片段的无穷证明系统，使得切割消除对应于公平终止。证明项是 LIN 的进程，这是一种具有（协）递归类型的线性 -演算变体，其中可以编码二元及（部分）多方会话。由此我们获得了 LIN（并通过其到 LIN 的编码间接为会话演算）的一个确保公平终止的行为类型系统：尽管良类型进程可能参与任意长的交互，但它们被公平地保证最终执行所有待处理动作。
引用
@article{arxiv.2207.03749,
title = {An Infinitary Proof Theory of Linear Logic Ensuring Fair Termination in the Linear $\pi$-Calculus},
author = {Luca Ciccone and Luca Padovani},
journal= {arXiv preprint arXiv:2207.03749},
year = {2022}
}