Sound and Complete Bisimilarities for Call-by-Name and Call-by-Value Lambda-mu Calculus

Résumé : Nous proposons les premières définitions de bisimilarités correctes et complètes pour le lambda-mu calcul non typé en appel par nom et en appel par valeur. Nous définissons une bisimilarité applicative pour chacune des sémantiques, et une bisimilarité environnementale en appel par nom. Nous donnons des examples d'équivalences pour montrer comment ces relations peuvent être utilisées ; en particulier, nous prouvons le contre-exemple de David et Py, qui ne peut être démontré avec la bisimilarité de forme normale définie auparavant par Lassen.
Type de document :
Rapport
[Research Report] RR-8447, INRIA. 2014
Liste complète des métadonnées


https://hal.inria.fr/hal-00926100
Contributeur : Sergueï Lenglet <>
Soumis le : mercredi 30 juillet 2014 - 11:45:38
Dernière modification le : jeudi 22 septembre 2016 - 14:32:09
Document(s) archivé(s) le : mardi 25 novembre 2014 - 21:00:35

Fichier

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

Identifiants

  • HAL Id : hal-00926100, version 2

Citation

Dariusz Biernacki, Sergueï Lenglet. Sound and Complete Bisimilarities for Call-by-Name and Call-by-Value Lambda-mu Calculus. [Research Report] RR-8447, INRIA. 2014. <hal-00926100v2>

Partager

Métriques

Consultations de
la notice

534

Téléchargements du document

414