Bisimulations for Delimited-Control Operators

Abstract : We propose a survey of the behavioral theory of an untyped lambda-calculus extended with the delimited-control operators shift and reset. We define a contextual equivalence for this calculus, that we then aim to characterize with coinductively defined relations, called bisimilarities. We study different styles of bisimilarities (namely applicative, normal form, and environmental), and we give several examples to illustrate their respective strengths and weaknesses. We also discuss how to extend this work to other delimited-control operators.
Type de document :
Rapport
[Research Report] RR-9096, Inria Nancy - Grand Est. 2017
Liste complète des métadonnées

Littérature citée [80 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01207112
Contributeur : Sergueï Lenglet <>
Soumis le : mercredi 20 septembre 2017 - 12:17:37
Dernière modification le : mardi 26 septembre 2017 - 15:26:31

Fichier

RR-9096.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01207112, version 3

Citation

Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk. Bisimulations for Delimited-Control Operators. [Research Report] RR-9096, Inria Nancy - Grand Est. 2017. 〈hal-01207112v3〉

Partager

Métriques

Consultations de
la notice

56

Téléchargements du document

7