一句话：提出项演算 pn，以细粒度方式刻画直觉主义线性逻辑证明网的静态结构与动态归约，并证明合流、强规范化等性质。
论文旨在为 Girard 的直觉主义线性逻辑证明网给出忠实且细粒度的计算解释。作者提出函数式项演算 pn：静态上定义 pn 项之间的等价关系，并证明其相对于证明网经典结构等价是可靠且完备的；动态上证明项演算中每个（指数）归约步都对应图形形式中一个不同的（指数）归约步，从而在项层面保持 Girard 证明网的归约粒度。作者还证明该演算满足合流、强规范化，保持 β-强规范化，并构造强互模拟来刻画具有相同图归约的 pn 项对。
This paper introduces a functional term calculus, called pn, that captures the essence of the operational semantics of Intuitionistic Linear Logic Proof-Nets with a faithful degree of granularity, both statically and dynamically. On the static side, we identify an equivalence relation on pn-terms which is sound and complete with respect to the classical notion of structural equivalence for proof-nets. On the dynamic side, we show that every single (exponential) step in the term calculus translates to a different single (exponential) step in the graphical formalism, thus capturing the original Girard’s granularity of proof-nets but on the level of terms. We also show some fundamental properties of the calculus such as confluence, strong normalization, preservation of β-strong normalization and the existence of a strong bisimulation that captures pairs of pn-terms having the same graph reduction.
@article{paperbot1570,
title = {A fine-grained computational interpretation of Girard’s intuitionistic proof-nets},
author = {Delia Kesner},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {POPL},
year = {2022},
doi = {10.1145/3498669}
}