论文标题
$λ$ -calculus在Hocore中的完全抽象的编码通过抽象机器
Fully Abstract Encodings of $λ$-Calculus in HOcore through Abstract Machines
论文作者
论文摘要
我们向Hocore介绍了逐个名称和呼叫$λ$ -CALCULUS的完全抽象编码，这是一个最小的高阶过程计算，没有名称限制。我们考虑了$λ$ -Calculus方面的几个等价 - 正常形式的双性异性，应用二比性和上下文等价 - 我们将其内部化为抽象机器，以证明编码的完全抽象。我们还证明，该技术将其缩放到$λμ$ -calculus，即带有控制运算符的$λ$ -calculus的标准扩展。
We present fully abstract encodings of the call-by-name and call-by-value $λ$-calculus into HOcore, a minimal higher-order process calculus with no name restriction. We consider several equivalences on the $λ$-calculus side -- normal-form bisimilarity, applicative bisimilarity, and contextual equivalence -- that we internalize into abstract machines in order to prove full abstraction of the encodings. We also demonstrate that this technique scales to the $λμ$-calculus, i.e., a standard extension of the $λ$-calculus with control operators.
