论文标题
互动的抽象机制（长版）
The Abstract Machinery of Interaction (Long Version)
论文作者
论文摘要
本文重新审视了Mackie和Danos＆Regnier引入的基于Girard的几何相互作用的机器，这是一台基于Girard的几何形状的机器。这是一台不寻常的机器，不依赖于线性逻辑网络上呈现的环境，其声音证明是复杂的，并经过了其他各种形式主义。在这里，我们根据Sands的改进，自然的分成概念提供了新的直接证明其正确性。此外，我们的证明是在IAM的新演示中进行的，该示例定义为直接作用于$λ$ - terms而不是线性逻辑证明网络的机器。
This paper revisits the Interaction Abstract Machine (IAM), a machine based on Girard's Geometry of Interaction, introduced by Mackie and Danos & Regnier. It is an unusual machine, not relying on environments, presented on linear logic proof nets, and whose soundness proof is convoluted and passes through various other formalisms. Here we provide a new direct proof of its correctness, based on a variant of Sands's improvements, a natural notion of bisimulation. Moreover, our proof is carried out on a new presentation of the IAM, defined as a machine acting directly on $λ$-terms, rather than on linear logic proof nets.
