TY - GEN
T1 - Strong bisimulation for control operators
AU - Kesner, Delia
AU - Bonelli, Eduardo
AU - Viso, Andrés
N1 - Publisher Copyright:
© Delia Kesner, Eduardo Bonelli, and Andrés Viso.
PY - 2020/1
Y1 - 2020/1
N2 - 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 λµ.
AB - 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 λµ.
KW - Lambda-mu calculus
KW - Proof-nets
KW - Strong bisimulation
UR - http://www.scopus.com/inward/record.url?scp=85078046019&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85078046019&partnerID=8YFLogxK
U2 - 10.4230/LIPIcs.CSL.2020.4
DO - 10.4230/LIPIcs.CSL.2020.4
M3 - Conference contribution
AN - SCOPUS:85078046019
T3 - Leibniz International Proceedings in Informatics, LIPIcs
BT - 28th EACSL Annual Conference on Computer Science Logic, CSL 2020
A2 - Fernandez, Maribel
A2 - Muscholl, Anca
T2 - 28th EACSL Annual Conference on Computer Science Logic, CSL 2020
Y2 - 13 January 2020 through 16 January 2020
ER -