Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt Generation

TL;DR

This paper develops sound and complete environmental bisimilarities for a calculus with multi-prompted delimited-control operators and dynamic prompt generation, advancing techniques for program equivalence proofs.

Contribution

It introduces a generalized framework for environmental bisimulations that handle multiple prompts, dynamic prompt generation, and evaluation contexts, with novel up-to techniques.

Findings

Established sound and complete bisimilarities for the calculus.

Generalized the framework to include evaluation contexts and continuations.

Enhanced bisimulation proofs with new up-to techniques.

Abstract

We present sound and complete environmental bisimilarities for a variant of Dybvig et al.'s calculus of multi-prompted delimited-control operators with dynamic prompt generation. The reasoning principles that we obtain generalize and advance the existing techniques for establishing program equivalence in calculi with single-prompted delimited control. The basic theory that we develop is presented using Madiot et al.'s framework that allows for smooth integration and composition of up-to techniques facilitating bisimulation proofs. We also generalize the framework in order to express environmental bisimulations that support equivalence proofs of evaluation contexts representing continuations. This change leads to a novel and powerful up-to technique enhancing bisimulation proofs in the presence of control operators.