[TYPES] Full abstraction of applicative contexts in call-by-value

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Dear all,

It is well-known that applicative bisimilarity is fully abstract on the
untyped call-by-value λ-calculus. A direct consequence of that is that
contextual equivalence can be restricted to applicative contexts (namely
contexts defined by the grammar E ::= [-] | Ev) leaving its discriminated
power unchanged. Such a result is, in principle, independent of applicative
bisimilarity and I was wondering if any of you is aware of any direct (i.e.
not going through applicative bisimilarity) proof that applicative contexts
suffice to characterise contextual equivalence.
Thanks a lot in advance!
Best,
Francesco Gavazzo and Ugo Dal Lago