\(\pi\)LL：协调线性逻辑、\(\pi\)-演算及其元理论

《ACM Transactions on Computational Logic》：\(\pi\)LL: Reconciling Linear Logic, the \(\pi\)-calculus, and their Metatheory

　　

摘要AI摘要

要查看此AI生成的摘要，您必须具有高级访问权限。

了解更多登录

摘要

摘要

Curry-Howard对应关系将自然演绎与$\lambda$-演算联系起来，这对类型化函数式语言产生了巨大的启发。这一研究由Abramsky在1994年发起，旨在为类型化并发语言寻找类似的基础，即通过线性逻辑[Girard 1987]与$\pi$-演算[Milner等人1992年]之间的联系来实现。

最近的进展在类型和语法层面建立了牢固的对应关系。线性命题对应于会话类型[Caires和Pfenning 2010；Wadler 2014]——这些类型规定了进程的可观察通信行为[Honda 1993]——而$\pi$-演算的基本运算符对应于用超序列表达的线性逻辑规则[Carbone等人2018；Kokke等人2019；Montesi和Peressotti 2018]。然而，在语义和元理论层面，情况尚不明确。以往研究中的语义和行为理论并不支持$\pi$-演算的前缀运算符。会话类型的操作语义尚未被重构，因此“会话忠实度”这一会话类型的标志性结果也尚未为“Proofs as Processes”理论所建立和证明。

在本文中，我们通过将标记转换系统及其同态的代数观点应用于线性逻辑的证明理论[Ciancia 2013]，仔细完善了“Proofs as Processes”的设计。由此产生的演算被称为$\pi$LL，它解决了之前的问题，并进一步展示了一个全面的元理论，将线性逻辑的证明理论与$\pi$-演算的行为理论联系起来。我们的发展明确了线性逻辑对进程可观察行为的保证属性。它还包括了一个关于进程内部工作原理的新原则，我们利用这一原理为使用线性逻辑类型化的进程建立了首个无死锁性和生产性的结果。

AI摘要

AI生成的摘要（实验性）

此摘要是由自动化工具生成的，并非由文章作者撰写或审阅。它旨在帮助读者发现内容、评估相关性，并辅助来自相关研究领域的读者理解本文。它作为对作者提供的摘要的补充，后者仍然是文章的官方摘要。完整文章才是权威版本。点击此处了解更多。

点击此处可以对摘要的准确性、清晰度和实用性进行评论。这样做将有助于改进未来的生成版本。

要查看此AI生成的简单语言摘要，您必须具有高级访问权限。