S. Arun-kumar and M. Hennessy, An efficiency preorder for processes, Acta Informatica, vol.29, pp.737-760, 1992.

H. P. Barendregt, The Lambda Calculus-Its Syntax and Semantics, 1984.

M. Berger, K. Honda, and N. Yoshida, Sequentiality and the pi-calculus, Proceedings of TLCA'01, pp.29-45, 2001.
DOI : 10.1007/3-540-45413-6_7
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.11.1716

M. Berger, K. Honda, and N. Yoshida, Genericity and the pi-calculus, Acta Informatica, vol.42, issue.2-3, pp.83-141, 2005.

M. Boreale and D. Sangiorgi, Some congruence properties for ?-calculus bisimilarities, Theoretical Computer Science, vol.198, pp.159-176, 1998.
DOI : 10.1016/s0304-3975(97)00125-4
URL : https://hal.archives-ouvertes.fr/inria-00073821

R. Demangeon and K. Honda, Full abstraction in a subtyped pi-calculus with linear types, Proceedings of CONCUR'11, vol.6901, pp.280-296, 2011.

M. Dezani-ciancaglini and E. Giovannetti, From Bohm's theorem to observational equivalences: an informal account, Electronic Notes in Theoretical Computer Science, vol.50, issue.2, pp.83-116, 2001.
DOI : 10.1016/s1571-0661(04)00167-7
URL : https://doi.org/10.1016/s1571-0661(04)00167-7

A. Durier, D. Hirschkoff, and D. Sangiorgi, Divergence and unique solution of equations, 16. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, vol.85, pp.1-11, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01643502

A. Durier, D. Hirschkoff, and D. Sangiorgi, Eager functions as processes, LICS 2018, 2018.
DOI : 10.1145/3209108.3209152
URL : https://hal.archives-ouvertes.fr/hal-01917255

J. R. Hindley and J. P. Seldin, Introduction to Combinators and ?-calculus, 1986.

D. Hirschkoff, J. Madiot, and D. Sangiorgi, Duality and i/o-types in the ?-calculus, Proceedings of CONCUR'12, vol.7454, pp.302-316, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00798028

R. Milner, Communication and Concurrency, 1989.

R. Milner, Functions as processes, Mathematical Structures in Computer Science, vol.2, issue.2, pp.119-141, 1990.
URL : https://hal.archives-ouvertes.fr/inria-00075405

R. Milner, Communicating and Mobile Systems: the ?-Calculus, 1999.

G. D. Plotkin, T ? as a universal domain, Journal of Computer and System Sciences, vol.17, pp.209-236, 1978.

D. Sangiorgi, An investigation into functions as processes, Proc. Ninth International Conference on the Mathematical Foundations of Programming Semantics (MFPS'93), vol.802, pp.143-159, 1993.

D. Sangiorgi, Typed pi-calculus at work: A correctness proof of jones's parallelisation transformation on concurrent objects, TAPOS, vol.5, issue.1, pp.25-33, 1999.

D. Sangiorgi, Language and Interaction: Essays in Honour of Robin Milner, Proof, 2000.

D. Sangiorgi, Introduction to Bisimulation and Coinduction, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00907026

D. Sangiorgi and D. Walker, The ?-calculus: a Theory of Mobile Processes, 2001.

D. Scott, Data types as lattices, SIAM Journal on Computing, vol.5, issue.3, pp.522-587, 1976.

N. Yoshida, K. Honda, and M. Berger, Let and ? be relations on agents of asynchronous ?-calculus with linear types. We assume, in addition to the untyped version, Journal of Logic and Algebraic Programming, vol.72, issue.2, pp.207-238, 2007.

, ? is an expansion relation and is a plain precongruence

, ) validates the up-to-?-and-contexts technique

, and ? validate rule ?