Strong Bisimulation for Control Operators.

The purpose of this paper is to identify programs with control operators whose reduction semantics are in exact correspondence. This is achieved by introducing a relation $\simeq$, defined over a revised presentation of Parigot's $\lambda\mu$-calculus we dub $\Lambda M$. Our result builds on three main ingredients which guide our semantical development: (1) factorization of Parigot's $\lambda\mu$-reduction into multiplicative and exponential steps by means of explicit operators, (2) adaptation of Laurent's original $\sigma$-equivalence to $\Lambda M$, and (3) interpretation of $\Lambda M$ into Laurent's polarized proof-nets (PPN). More precisely, we first give a translation of $\Lambda M$-terms into PPN which simulates the reduction relation of our calculus into cut elimination of PPN. Second, we establish a precise relation between our relation $\simeq$ and Laurent's $\sigma$-equivalence for $\lambda\mu$-terms. Moreover, $\simeq$ is shown to characterize structural equivalence in PPN. Most notably, $\simeq$ is shown to be a strong bisimulation with respect to reduction in $\Lambda M$, \ie two $\simeq$-equivalent terms have the exact same reduction semantics, a result which fails for Regnier's $\sigma$-equivalence in $\lambda$-calculus as well as for Laurent's $\sigma$-equivalence in $\lambda\mu$.