Applicative Bisimilarities for Call-by-Name and Call-by-Value λμ-Calculus

Abstract : We propose the first sound and complete bisimilarities for the call-by-name and call-by-value untyped λµ-calculus, defined in the applicative style. We give equivalence examples to illustrate how our relations can be used; in particular, we prove David and Py's counter-example, which cannot be proved with Lassen's preexisting normal form bisimilarities for the λµ-calculus.
Type de document :
Communication dans un congrès
Mathematical Foundations of Programming Semantics Thirtieth Conference, Jun 2014, Ithaca, United States. 308, pp.49 - 64, 2014, 〈10.1016/j.entcs.2014.10.004〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01080960
Contributeur : Sergueï Lenglet <>
Soumis le : jeudi 6 novembre 2014 - 15:33:17
Dernière modification le : jeudi 11 janvier 2018 - 06:25:24
Document(s) archivé(s) le : samedi 7 février 2015 - 11:06:29

Fichier

lambdamuentcs.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Dariusz Biernacki, Sergueï Lenglet. Applicative Bisimilarities for Call-by-Name and Call-by-Value λμ-Calculus. Mathematical Foundations of Programming Semantics Thirtieth Conference, Jun 2014, Ithaca, United States. 308, pp.49 - 64, 2014, 〈10.1016/j.entcs.2014.10.004〉. 〈hal-01080960〉

Partager

Métriques

Consultations de la notice

179

Téléchargements de fichiers

108