[TYPES] Observational equivalence decision

[Stephane Gimenez]

Hi,

I'm working in the context of simply-typed lambda calculus with
call-by-value semantics. And, I would like to know what are the best
known algorithms that (partially) decide observational equivalence of
two terms in this context.
(any definition of observational equivalence could suit).

Can anyone give me pointers to written material?

Thanks,
Stéphane.