We present fully abstract encodings of the call-by-name and call-by-value $\lambda$-calculus into HOcore, a minimal higher-order process calculus with no name restriction. We consider several equivalences on the $\lambda$-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 $\lambda\mu$-calculus, i.e., a standard extension of the $\lambda$-calculus with control operators.

翻译：我们提出了按名调用和按值调用$λ$-演算在HOcore中的完全抽象编码。HOcore是一种最小的无名称限制的高阶进程演算。我们考虑了$λ$-演算侧的几种等价关系——范式互模拟、应用互模拟和上下文等价——并将这些等价关系内化到抽象机器中，以证明编码的完全抽象性。我们还展示了该技术可扩展到$λμ$-演算，即$λ$-演算带有控制算子的标准扩展。