论文标题
线性逻辑的无限证明理论，确保在线性$π$ -calculus中公平终止
An Infinitary Proof Theory of Linear Logic Ensuring Fair Termination in the Linear $π$-Calculus
论文作者
论文摘要
公平终止是可能“原则上”不同但在“实践中终止”的计划的属性，即在适当的公平性假设下关于解决非确定性选择的假设。我们研究了$μ$ MALL $^\ infty $的保守扩展，这是线性逻辑的乘法添加剂片段的无限证明系统，最少和最大的固定点，因此切割消除对应于公平终止。证明术语是$π$ lin的过程，这是线性$π$ -calculus的变体，该变体具有（CO）递归类型，可以在其中编码二进制和（某些）多方会话。结果，我们获得了$π$ lin的行为类型系统（并通过将其编码为$π$ lin间接进行calculi），以确保公平终止：尽管良好的过程可能会进行任意长时间的互动，但它们可以公平地保证最终执行所有悬而未决的操作。
Fair termination is the property of programs that may diverge "in principle" but that terminate "in practice", i.e. under suitable fairness assumptions concerning the resolution of non-deterministic choices. We study a conservative extension of $μ$MALL$^\infty$, the infinitary proof system of the multiplicative additive fragment of linear logic with least and greatest fixed points, such that cut elimination corresponds to fair termination. Proof terms are processes of $π$LIN, a variant of the linear $π$-calculus with (co)recursive types into which binary and (some) multiparty sessions can be encoded. As a result we obtain a behavioral type system for $π$LIN (and indirectly for session calculi through their encoding into $π$LIN) that ensures fair termination: although well-typed processes may engage in arbitrarily long interactions, they are fairly guaranteed to eventually perform all pending actions.
