Normal Form Bisimulations for Delimited-Control Operators

Abstract : We define a notion of normal form bisimilarity for the un-typed call-by-value λ-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.
Type de document :
Communication dans un congrès
T. Shrijvers and P. Thiemann. Symposium on Functional and Logic Programming (FLOPS 2012), Jun 2012, Kobé, Japan. Springer, LNCS 7294, pp.47 - 61, 2012, 〈10.1007/978-3-642-29822-6_7〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01399951
Contributeur : Sergueï Lenglet <>
Soumis le : lundi 21 novembre 2016 - 11:08:00
Dernière modification le : mercredi 30 novembre 2016 - 14:14:00
Document(s) archivé(s) le : mardi 21 mars 2017 - 00:56:59

Fichier

biernacki-lenglet-flops12.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Dariusz Biernacki, Sergueï Lenglet. Normal Form Bisimulations for Delimited-Control Operators. T. Shrijvers and P. Thiemann. Symposium on Functional and Logic Programming (FLOPS 2012), Jun 2012, Kobé, Japan. Springer, LNCS 7294, pp.47 - 61, 2012, 〈10.1007/978-3-642-29822-6_7〉. 〈hal-01399951〉

Partager

Métriques

Consultations de la notice

16

Téléchargements de fichiers

36