一句话：将带最小/最大不动点的子结构逻辑循环证明解释为会话类型进程，并给出可判定的局部有效性条件。
本文在直觉主义线性逻辑与会话类型 pi-演算的 Curry-Howard 对应基础上，研究带最小和最大不动点的子结构逻辑片段。作者把由此产生的无穷证明系统赋予计算解释，将其视为会话类型化进程，并针对互递归进程提出一种有效可判定的局部有效性条件，以识别对应 Fortier 与 Santocanale 意义下有效循环证明的项。该条件比 Fortier 与 Santocanale 的卫式条件更严格，但具有局部性和组合性，因而更适合作为编程语言的基础。结果显示循环证明与互递归可作为进程语言中的类型化构造，同时保持可判定检查。
Proof theory provides a foundation for studying and reasoning about programming languages, most directly based on the well-known Curry-Howard isomorphism between intuitionistic logic and the typed lambda-calculus. More recently, a correspondence between intuitionistic linear logic and the session-typed pi-calculus has been discovered. In this paper, we establish an extension of the latter correspondence for a fragment of substructural logic with least and greatest fixed points. We describe the computational interpretation of the resulting infinitary proof system as session-typed processes, and provide an effectively decidable local criterion to recognize mutually recursive processes corresponding to valid circular proofs as introduced by Fortier and Santocanale. We show that our algorithm imposes a stricter requirement than Fortier and Santocanale's guard condition, but is local and compositional and therefore more suitable as the basis for a programming language.
@article{paperbot1704,
title = {Circular Proofs as Session-Typed Processes: A Local Validity Condition},
author = {Farzaneh Derakhshan and Frank Pfenning},
journal = {Logical Methods in Computer Science},
volume = {Volume 18, Issue 2},
year = {2022},
doi = {10.46298/lmcs-18(2:8)2022}
}