Applicative Bisimilarities for Call-by-Name and Call-by-Value λμ-Calculus
Résumé
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.
Domaines
Informatique [cs]
Origine : Fichiers produits par l'(les) auteur(s)
Loading...