Applicative Bisimilarities for Call-by-Name and Call-by-Value λμ-Calculus
Dariusz Biernacki, Sergueï Lenglet · Electronic Notes in Theoretical Computer Science · 2014
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.