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是一种无名称限制的最小高阶进程演算。我们在λ演算侧考虑了多种等价关系——范式互模拟、应用互模拟和上下文等价——通过将这些等价关系内化到抽象机中，从而证明编码的完全抽象性。我们还证明了该技术可扩展至λμ演算，即带有控制算子的λ演算标准扩展形式。