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

We propose the first sound and complete bisimilarities for the call-by-name and call-by-value untyped lambda-mu calculus. We define applicative bisimilarities for both semantics and environmental bisimilarity for call-by-name. 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 lambda-mu calculus.; 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.