Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH scholarly article en Kesner, Delia; Bonelli, Eduardo; Viso, Andrés License: Creative Commons Attribution 3.0 Unported license (CC-BY 3.0)
when quoting this document, please refer to the following
URN: urn:nbn:de:0030-drops-116473

; ;

Strong Bisimulation for Control Operators (Invited Talk)



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 ≃, defined over a revised presentation of Parigot’s λμ-calculus we dub ΛM.
Our result builds on two fundamental ingredients: (1) factorization of λμ-reduction into multiplicative and exponential steps by means of explicit term operators of ΛM, and (2) translation of ΛM-terms into Laurent’s polarized proof-nets (PPN) such that cut-elimination in PPN simulates our calculus. Our proposed relation ≃ is shown to characterize structural equivalence in PPN. Most notably, ≃ is shown to be a strong bisimulation with respect to reduction in ΛM, i.e. two ≃-equivalent terms have the exact same reduction semantics, a result which fails for Regnier’s σ-equivalence in λ-calculus as well as for Laurent’s σ-equivalence in λμ.

BibTeX - Entry

  author =	{Delia Kesner and Eduardo Bonelli and Andr{\'e}s Viso},
  title =	{{Strong Bisimulation for Control Operators (Invited Talk)}},
  booktitle =	{28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
  pages =	{4:1--4:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-132-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{152},
  editor =	{Maribel Fern{\'a}ndez and Anca Muscholl},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{},
  URN =		{urn:nbn:de:0030-drops-116473},
  doi =		{10.4230/LIPIcs.CSL.2020.4},
  annote =	{Keywords: Lambda-mu calculus, proof-nets, strong bisimulation}

Keywords: Lambda-mu calculus, proof-nets, strong bisimulation
Seminar: 28th EACSL Annual Conference on Computer Science Logic (CSL 2020)
Issue date: 2020
Date of publication: 06.01.2020

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI