Strong bisimulation for control operators

Delia Kesner, Eduardo Bonelli, Andrés Viso

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

2 Scopus citations

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 ', 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 λµ.

Original languageEnglish
Title of host publication28th EACSL Annual Conference on Computer Science Logic, CSL 2020
EditorsMaribel Fernandez, Anca Muscholl
ISBN (Electronic)9783959771320
DOIs
StatePublished - Jan 2020
Event28th EACSL Annual Conference on Computer Science Logic, CSL 2020 - Barcelona, Spain
Duration: 13 Jan 202016 Jan 2020

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume152
ISSN (Print)1868-8969

Conference

Conference28th EACSL Annual Conference on Computer Science Logic, CSL 2020
Country/TerritorySpain
CityBarcelona
Period13/01/2016/01/20

Keywords

  • Lambda-mu calculus
  • Proof-nets
  • Strong bisimulation

Fingerprint

Dive into the research topics of 'Strong bisimulation for control operators'. Together they form a unique fingerprint.

Cite this