  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 $\simeq_\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 via cut elimination
of PPN. Second, we establish a precise correspondence between our relation
$\simeq$ and Laurent's $\simeq_\sigma$-equivalence for $\lambda\mu$-terms.
Moreover, $\simeq$-equivalent terms translate to structurally equivalent PPN.
Most notably, $\simeq$ is shown to be a strong bisimulation with respect to
reduction in $\Lambda M$, i.e. two $\simeq$-equivalent terms have the exact
same reduction semantics, a result which fails for Regnier's
$\simeq_\sigma$-equivalence in $\lambda$-calculus as well as for Laurent's
$\simeq_\sigma$-equivalence in $\lambda\mu$.
