一句话：通过抽象机将按名/按值 λ-演算及 λμ-演算完全抽象地编码到最小高阶进程演算 HOcore。
本文研究如何将按名与按值 λ-演算编码到 HOcore——一种不含名字限制的最小高阶进程演算，并证明该编码是完全抽象的。作者考虑 λ-演算侧的范式双模拟、应用双模拟与上下文等价，通过将这些等价关系内化到抽象机中，建立编码保持并反射行为的证明方法。该技术进一步扩展到带控制算子的 λμ-演算。结果表明，抽象机可作为研究进程演算编码完全抽象性的有效工具，并为 λ-演算及其控制算子扩展在 HOcore 中给出完全抽象编码。
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.
@article{paperbot2746,
title = {Fully Abstract Encodings of $\lambda$-Calculus in HOcore through Abstract Machines},
author = {Małgorzata Biernacka and Dariusz Biernacki and Sergueï Lenglet and Piotr Polesiuk and Damien Pous and Alan Schmitt},
journal = {Logical Methods in Computer Science},
volume = {Volume 20, Issue 3},
year = {2024},
doi = {10.46298/lmcs-20(3:3)2024}
}