Effectful applicative similarity for call-by-name lambda calculi (Q1989333)

The authors introduce and discuss a notion of equivalence of terms for a call-by-name lambda calculus with algebraic operations. This notion of applicative similarity is based on interpreting terms and operations as monadic values and is able to fully characterise contextual equivalence of terms (Corollary 1 on full abstraction). This contrasts with the usual notion of applicative similarity that interprets terms as values, but not monadic ones, and that does not satisfy full abstration with respect to contextual equivalence.