Logotipo ImpactU
Autor

Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt Generation

Acceso Abierto
ID Minciencias: ART-0001554950-21
Ranking: ART-ART_A2

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.

Tópico:

Logic, programming, and type systems

Citaciones:

Citations: 11
11

Citaciones por año:

Altmétricas:

Paperbuzz Score: 0
0

Información de la Fuente:

FuentearXiv (Cornell University)
Cuartil año de publicaciónNo disponible
VolumenNo disponible
IssueNo disponible
PáginasNo disponible
pISSNNo disponible
ISSNNo disponible

Enlaces e Identificadores:

Scienti ID0001554950-21Minciencias IDART-0001554950-21Open_access URLhttps://arxiv.org/abs/1611.09626
Doi URLhttps://doi.org/10.48550/arxiv.1611.09626Openalex URLhttps://openalex.org/W3105695071
Artículo de revista