A fully-abstract semantics of lambda-mu in the pi-calculus

TL;DR

This paper presents a fully-abstract, compositional semantics for the lambda-mu-calculus extended with explicit substitution, interpreted into a pi-calculus variant, establishing equivalence of multiple weak reduction notions and full abstraction results.

Contribution

It introduces a novel interpretation of lambda-mu with explicit substitution into pi-calculus, unifying various weak equivalences and proving full abstraction.

Findings

All four weak equivalence notions coincide.

The interpretation preserves single-step explicit head reduction.

Full abstraction holds for the interpretation with respect to weak bisimilarity.

Abstract

We study the lambda-mu-calculus, extended with explicit substitution, and define a compositional output-based interpretation into a variant of the pi-calculus with pairing that preserves single-step explicit head reduction with respect to weak bisimilarity. We define four notions of weak equivalence for lambda-mu -- one based on weak reduction, two modelling weak head-reduction and weak explicit head reduction (all considering terms without weak head-normal form equivalent as well), and one based on weak approximation -- and show they all coincide. We will then show full abstraction results for our interpretation for the weak equivalences with respect to weak bisimilarity on processes.