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

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

https://hal.inria.fr/hal-00926100
Contributeur : Sergueï Lenglet <>
Soumis le : mercredi 30 juillet 2014 - 11:45:38
Dernière modification le : jeudi 11 janvier 2018 - 06:25:24
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

568

Téléchargements de fichiers

464