A. Ahmed, D. Dreyer, and A. Rossberg, State-dependent representation independence, Proceedings of the Thirty-Fifth Annual ACM Symposium on Principles of Programming Languages, pp.340-353, 2009.

A. Aristizábal, D. Biernacki, S. Lenglet, and P. Polesiuk, Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt Generation, Logical Methods in Computer Science, vol.13, issue.3, 2017.

D. Biernacki, S. Lenglet, and P. Polesiuk, Proving soundness of extensional normalform bisimilarities, Proceedings of the 33th Annual Conference on Mathematical Foundations of Programming Semantics, vol.336, pp.41-56, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01650000

D. Biernacki, S. Lenglet, and P. Polesiuk, A complete normal-form bisimilarity for state, 2019.
URL : https://hal.archives-ouvertes.fr/hal-02002115

D. Dreyer, G. Neis, and L. Birkedal, The impact of higher-order state and control effects on local relational reasoning, Journal of Functional Programming, vol.22, issue.4-5, pp.477-528, 2012.

G. Jaber and N. Tabareau, Kripke open bisimulation -A marriage of game semantics and operational techniques, Programming Languages and Systems -13th Asian Symposium, vol.9458, pp.271-291, 2015.

R. Jagadeesan, C. Pitcher, and J. Riely, Open bisimulation for aspects, Trans. Aspect-Oriented Software Development, vol.5, pp.72-132, 2009.

V. Koutavas, P. B. Levy, and E. Sumii, From applicative to environmental bisimulation, Proceedings of the 27th Annual Conference on Mathematical Foundations of Programming Semantics, vol.276, pp.215-235, 2011.

V. Koutavas and M. Wand, Small bisimulations for reasoning about higher-order imperative programs, POPL'06, pp.141-152, 2006.

J. Laird, A fully abstract trace semantics for general references, Automata, Languages and Programming, 34th International Colloquium, vol.4596, pp.667-679, 2007.

S. B. Lassen, Eager normal form bisimulation, LICS'05, pp.345-354, 2005.

J. Madiot, D. Pous, and D. Sangiorgi, Bisimulations up-to: Beyond first-order transition systems, 25th International Conference on Concurrency Theory, vol.8704, pp.93-108, 2014.
URL : https://hal.archives-ouvertes.fr/hal-00990859

A. S. Murawski and N. Tzevelekos, Game semantics for good general references, Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011, pp.75-84, 2011.

A. S. Murawski and N. Tzevelekos, Algorithmic games for full ground references, Formal Methods in System Design, vol.52, issue.3, pp.277-314, 2018.

A. Pitts and I. Stark, Operational reasoning for functions with local state, Higher Order Operational Techniques in Semantics, pp.227-273, 1998.

D. Sangiorgi, The lazy lambda calculus in a concurrency scenario, LICS'92, pp.102-109, 1992.

D. Sangiorgi, N. Kobayashi, and E. Sumii, Environmental bisimulations for higherorder languages, ACM Transactions on Programming Languages and Systems, vol.33, issue.1, pp.1-69, 2011.
URL : https://hal.archives-ouvertes.fr/hal-01337665

K. Støvring and S. B. Lassen, A complete, co-inductive syntactic theory of sequential control and state, SIGPLAN Notices, vol.42, issue.1, pp.161-172, 2007.

E. Sumii, A complete characterization of observational equivalence in polymorphic lambda-calculus with general references, Computer Science Logic, 23rd international Workshop, vol.5771, pp.455-469, 2009.