A Syntactic Method for Proving Observational Equivalences

Martin Odersky

Research Report YALEU/DCS/RR-964
Department of Compter Science, Yale University
May 1993


We present a syntactic method for proving observational
equivalences in reduction systems. The method is based on establishing
a weak diamond property for critical pairs. It has been used
successfully in proofs on the observational equivalence theories of
$\lambda_{var}$ and $\lambda\nu$.