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

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.