Normal form bisimulations for delimited-control operators

DOI10.1007/978-3-642-29822-6_7MaRDI QIDQ2900257zbMATH OpenOpenAlexFDO

Authors Dariusz Biernacki, Sergueï Lenglet

Publication date 20 July 2012

Published in Functional and Logic Programming (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1202.5959

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Functional programming and lambda calculus (68N18)

Abstract: We define a notion of normal form bisimilarity for the untyped call-by-value lambda calculus extended with the delimited-control operators shift and reset. Normal form bisimilarities are simple, easy-to-use behavioral equivalences which relate terms without having to test them within all contexts (like contextual equivalence), or by applying them to function arguments (like applicative bisimilarity). We prove that the normal form bisimilarity for shift and reset is sound but not complete w.r.t. contextual equivalence and we define up-to techniques that aim at simplifying bisimulation proofs. Finally, we illustrate the simplicity of the techniques we develop by proving several equivalences on terms.

Recommendations

• Bisimulations for delimited-control operators
• Applicative bisimulations for delimited-control operators
• Proving soundness of extensional normal-form bisimilarities
• Environmental bisimulations for delimited-control operators
• A sound and complete bisimulation for contextual equivalence in -calculus with call/cc

Cited in

(15)

• Proving soundness of extensional normal-form bisimilarities
• Applicative bisimulations for delimited-control operators
• Environmental bisimulations for delimited-control operators
• A sound and complete bisimulation for contextual equivalence in -calculus with call/cc
• A Complete, Co-inductive Syntactic Theory of Sequential Control and State
• Typed Normal Form Bisimulation
• Normal Bisimulations in Calculi with Passivation
• Environmental bisimulations for delimited-control operators with dynamic prompt generation
• Environmental bisimulations for delimited-control operators with dynamic prompt generation
• Proving soundness of extensional normal-form bisimilarities
• Bisimulations for delimited-control operators
• THEORETICAL PEARL: A simple proof of a folklore theorem about delimited control
• Effectful normal form bisimulation
• Fully abstract normal form bisimulation for call-by-value PCF
• Pushdown normal-form bisimulation: a nominal context-free approach to program equivalence

This page was built for publication: Normal form bisimulations for delimited-control operators

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2900257)