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}
}