Małgorzata Biernacka ; Dariusz Biernacki ; Sergueï Lenglet ; Piotr Polesiuk ; Damien Pous et al.
-
Fully Abstract Encodings of $\lambda$-Calculus in HOcore through
Abstract Machines
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.