A. Ahmed, D. Dreyer, and A. Rossberg, State-dependent representation independence, POPL'09, pp.340-353, 2009.

N. Bohr and L. Birkedal, Relational Reasoning for Recursive Types and References, APLAS'06, pp.79-96, 2006.
DOI : 10.1007/11924661_5

A. Carayol, D. Hirschkoff, and D. Sangiorgi, On the representation of McCarthy's <mml:math altimg="si1.gif" overflow="scroll" xmlns:xocs="http://www.elsevier.com/xml/xocs/dtd" xmlns:xs="http://www.w3.org/2001/XMLSchema" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns="http://www.elsevier.com/xml/ja/dtd" xmlns:ja="http://www.elsevier.com/xml/ja/dtd" xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:tb="http://www.elsevier.com/xml/common/table/dtd" xmlns:sb="http://www.elsevier.com/xml/common/struct-bib/dtd" xmlns:ce="http://www.elsevier.com/xml/common/dtd" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:cals="http://www.elsevier.com/xml/common/cals/dtd"><mml:mi mathvariant="italic">amb</mml:mi></mml:math> in the <mml:math altimg="si2.gif" overflow="scroll" xmlns:xocs="http://www.elsevier.com/xml/xocs/dtd" xmlns:xs="http://www.w3.org/2001/XMLSchema" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns="http://www.elsevier.com/xml/ja/dtd" xmlns:ja="http://www.elsevier.com/xml/ja/dtd" xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:tb="http://www.elsevier.com/xml/common/table/dtd" xmlns:sb="http://www.elsevier.com/xml/common/struct-bib/dtd" xmlns:ce="http://www.elsevier.com/xml/common/dtd" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:cals="http://www.elsevier.com/xml/common/cals/dtd"><mml:mi>??</mml:mi></mml:math>-calculus, Theoretical Computer Science, vol.330, issue.3, pp.439-473, 2005.
DOI : 10.1016/j.tcs.2004.10.005

D. Nicola and M. Hennessy, Testing equivalences for processes, Theoretical Computer Science, vol.34, issue.1-2, pp.83-133, 1984.
DOI : 10.1016/0304-3975(84)90113-0

C. Fournet, F. Le-fessant, L. Maranget, and A. Schmitt, JoCaml: A Language for Concurrent Distributed and Mobile Programming, Advanced Functional Programming, pp.129-158, 2002.
DOI : 10.1007/978-3-540-44833-4_5

. Gorla, Towards a unified approach to encodability and separation results for process calculi. CONCUR '08, pp.492-507, 2008.

A. Jeffrey and J. Rathke, A theory of bisimulation for a fragment of Concurrent ML with local names, Proceedings Fifteenth Annual IEEE Symposium on Logic in Computer Science (Cat. No.99CB36332), pp.1-48, 2004.
DOI : 10.1109/LICS.2000.855780

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

X. Leroy and S. Blazy, Formal Verification of a C-like Memory Model and Its Uses for Verifying Program Transformations, Journal of Automated Reasoning, vol.17, issue.5???6, pp.1-31, 2008.
DOI : 10.1007/s10817-008-9099-0
URL : https://hal.archives-ouvertes.fr/inria-00289542

B. Liskov and L. Shrira, Promises: linguistic support for efficient asynchronous procedure calls in distributed systems, pp.260-267, 1988.

J. Niehren, J. Schwinghammer, and G. Smolka, A concurrent lambda calculus with futures, Theoretical Computer Science, vol.364, issue.3, pp.338-356, 2006.
DOI : 10.1016/j.tcs.2006.08.016
URL : https://hal.archives-ouvertes.fr/inria-00090434

J. Niehren, D. Sabel, M. Schmidt-schauß, and J. Schwinghammer, Observational Semantics for a Concurrent Lambda Calculus with Reference Cells and Futures, Electronic Notes in Theoretical Computer Science, vol.173, pp.313-337, 2007.
DOI : 10.1016/j.entcs.2007.02.041
URL : https://hal.archives-ouvertes.fr/inria-00128861

C. L. Ong, Non-determinism in a functional setting, [1993] Proceedings Eighth Annual IEEE Symposium on Logic in Computer Science, pp.275-286, 1993.
DOI : 10.1109/LICS.1993.287580

J. Parrow, Expressiveness of Process Algebras, Electronic Notes in Theoretical Computer Science, vol.209, pp.173-186, 2008.
DOI : 10.1016/j.entcs.2008.04.011

U. S. Reddy and H. Yang, Correctness of data representations involving heap data structures, Sci. Comput. Program, vol.50, pp.1-3129, 2004.

A. Rensink and W. Vogler, Fair testing, Information and Computation, vol.205, issue.2, pp.125-198, 2007.
DOI : 10.1016/j.ic.2006.06.002

J. H. Reppy, Concurrent Programming in ML, 1999.
DOI : 10.1017/CBO9780511574962

J. C. Reynolds, Types, abstraction, and parametric polymorphism, Information Processing '83, pp.513-523, 1983.

J. G. Riecke, Fully abstract translations between functional languages, POPL'91, pp.245-254, 1991.

E. Ritter and A. M. Pitts, A fully abstract translation between a lambdacalculus with reference types and standard ml, TLCA'95, 1995.

D. Sabel and M. Schmidt-schauß, A call-by-need lambda calculus with locally bottom-avoiding choice: context lemma and correctness of transformations, Mathematical Structures in Computer Science, vol.1672, issue.03, pp.501-553, 2008.
DOI : 10.1017/S0956796897002967

M. Schmidt-schauß, J. Niehren, D. Sabel, and J. Schwinghammer, Adequacy of Compositional Translations for Observational Semantics, 5th IFIP, IFIP 273, pp.521-535, 2008.
DOI : 10.1007/978-0-387-09680-3_35

M. Schmidt-schauß and D. Sabel, On generic context lemmas for lambda calculi with sharing. Frank report 27, Inst. f. Informatik, J.W.Goethe- University, 2007.

M. Schmidt-schauß, J. Niehren, J. Schwinghammer, and D. Sabel, Adequacy of Compositional Translations for Observational Semantics, Inst. f. Informatik, J.W.Goethe-University, 2009.
DOI : 10.1007/978-0-387-09680-3_35

J. Schwinghammer, D. Sabel, J. Niehren, and M. Schmidt-schauß, On correctness of buffer implementations in a concurrent lambda calculus with futures, 2009.