A complete characterization of observational equivalence in polymorphic λ-calculus with general references

Abstract

We give the first sound and complete proof method for observational equivalence in full polymorphic λ-calculus with existential types and first-class, higher-order references. Our method is syntactic and elementary in the sense that it only employs simple structures such as relations on terms. It is nevertheless powerful enough to prove many interesting equivalences that can and cannot be proved by previous approaches, including the latest work by Ahmed, Dreyer and Rossberg (POPL 2009). © 2009 Springer Berlin Heidelberg.