一句话：通过抽象机证明 call-by-name λ-演算到 HOcore 的完全抽象编码，并统一多种等价关系。
论文为 call-by-name λ-演算给出了到 HOcore 的完全抽象编码，其中 HOcore 是一种不带名字限制的最小高阶进程演算。问题在于如何让编码不仅保持计算行为，还能精确反映源语言的等价关系。为此，作者在 λ-演算侧考察正规形式互模拟、应用型互模拟和上下文等价，并将这些等价内化到抽象机中，以证明编码的完全抽象性。结果表明，所构造的编码能够保持并反映上述多种等价关系，说明 HOcore 足以精确刻画 call-by-name λ-演算的可观察行为。
We present fully abstract encodings of the call-by-name λ-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.
@inproceedings{paperbot4216,
title = {Fully abstract encodings of λ-calculus in HOcore through abstract machines},
author = {Malgorzata Biernacka and Dariusz Biernacki and Serguei Lenglet and Piotr Polesiuk and Damien Pous and Alan Schmitt},
booktitle = {LICS},
year = {2017},
doi = {10.1109/lics.2017.8005118}
}