Fully Abstract Encodings of -Calculus in HOcore through Abstract Machines

We present fully abstract encodings of the call-by-name and call-by-value -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 of the encodings. We also demonstrate that this technique scales to the -calculus, i. e. , a standard extension of the -calculus with control operators.