论文标题
在线性金属含量中进行会话类型的过程的强劲进步，并具有圆形证明
Strong Progress for Session-Typed Processes in a Linear Metalogic with Circular Proofs
论文作者
论文摘要
我们引入了最少和最大的固定点的无限一阶线性逻辑。为了确保削减消除，我们对无限推导施加了有效性条件。我们的演算旨在理解相互定义的电感和共同诱导线性谓词的丰富特征。在一个主要案例研究中，我们使用它来证明在异步传播语义下二进制会话类型过程的强大进步属性。据我们所知，这是该属性的第一个证明。
We introduce an infinitary first order linear logic with least and greatest fixed points. To ensure cut elimination, we impose a validity condition on infinite derivations. Our calculus is designed to reason about rich signatures of mutually defined inductive and coinductive linear predicates. In a major case study we use it to prove the strong progress property for binary session-typed processes under an asynchronous communication semantics. As far as we are aware, this is the first proof of this property.
