We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.LO

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Logic in Computer Science

Title: Strong Bisimulation for Control Operators

Abstract: 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 two fundamental ingredients: (1) factorization of $\lambda\mu$-reduction into multiplicative and exponential steps by means of explicit term operators of $\Lambda M$, and (2) translation of $\Lambda M$-terms into Laurent's polarized proof-nets (PPN) such that cut-elimination in PPN simulates our calculus. Our proposed relation $\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$, i.e. 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$.
Subjects: Logic in Computer Science (cs.LO); Programming Languages (cs.PL)
DOI: 10.4230/LIPIcs.CSL.2020.4
Cite as: arXiv:1906.09370 [cs.LO]
  (or arXiv:1906.09370v2 [cs.LO] for this version)

Submission history

From: Andrés Ezequiel Viso [view email]
[v1] Sat, 22 Jun 2019 02:35:39 GMT (107kb)
[v2] Wed, 16 Oct 2019 15:11:34 GMT (166kb,D)

Link back to: arXiv, form interface, contact.