Fully Abstract Encodings of $\lambda$-Calculus in HOcore through Abstract Machines

TL;DR

This paper develops fully abstract encodings of call-by-name and call-by-value lambda calculus into HOcore, a minimal process calculus, using abstract machines to prove full abstraction and extending the approach to lambda-mu calculus.

Contribution

It introduces a novel method to achieve full abstraction of lambda calculus encodings into HOcore via abstract machines, scalable to lambda-mu calculus.

Findings

Successful encoding of lambda calculus into HOcore with full abstraction.

Scalability of the encoding technique to lambda-mu calculus.

Internalization of various equivalences into abstract machines.

Abstract

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.