[. Bibliography, P. Accattoli, D. Barenbaum, and . Mazza, Distilling abstract machines, Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, pp.363-376, 2014.

S. Abramsky, A. , and G. Costa, The lazy ?-calculus Distributive semantics for nondeterministic typed lambda-calculi, Research Topics in Functional Programming, pp.65-117121, 1984.

P. Arrighi and G. Dowek, Linear-algebraic lambda-calculus: higher-order, encodings, and confluence, Rewriting Techniques and Applications, 19th International Conference Proceedings, pp.17-31, 2008.

P. Arrighi and A. Díaz-caro, A System F accounting for scalars, Logical Methods in Computer Science, vol.8, issue.1, p.2012
DOI : 10.2168/LMCS-8(1:11)2012

URL : https://hal.archives-ouvertes.fr/hal-00924944

P. Arrighi, A. Díaz-caro, and B. Valiron, The vectorial lambda-calculus. CoRR, abs, 1138.
URL : https://hal.archives-ouvertes.fr/hal-00921087

[. Accattoli and U. D. Lago, Beta reduction is invariant, indeed, Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, pp.1-8, 2014.
DOI : 10.1145/2603088.2603105

URL : https://hal.archives-ouvertes.fr/hal-01091551

M. Alberti, Normal forms for the algebraic lambda-calculus
URL : https://hal.archives-ouvertes.fr/hal-00779911

S. Abramsky and C. Ong, Full Abstraction in the Lazy Lambda Calculus, Information and Computation, vol.105, issue.2, pp.159-267, 1993.
DOI : 10.1006/inco.1993.1044

[. Barendregt, The Lambda Calculus ? Its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics, 1984.

P. Buiras, A. Díaz-caro, and M. Jaskelioff, Confluence via strong normalisation in an algebraic ??-calculus with rewriting, Proceedings of the 6th Workshop on Logical and Semantic Frameworks with Applications, pp.16-29, 2011.
DOI : 10.4204/EPTCS.81.2

URL : https://hal.archives-ouvertes.fr/hal-00924938

[. Bernardo, R. D. Nicola, and M. Loreti, A uniform framework for modeling nondeterministic, probabilistic, stochastic, or mixed processes and their behavioral equivalences, Information and Computation, vol.225, pp.29-82, 2013.
DOI : 10.1016/j.ic.2013.02.004

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.678.1180

C. [. Boudol and . Laneve, The Discriminating Power of Multiplicities in the??-Calculus, Information and Computation, vol.126, issue.1, pp.83-102, 1996.
DOI : 10.1006/inco.1996.0037

URL : https://hal.archives-ouvertes.fr/inria-00074234

G. Boudol, The lambda-calculus with multiplicities (abstract)

G. Boudol, Lambda-Calculi for (Strict) Parallel Functions, Information and Computation, vol.108, issue.1, pp.51-127, 1994.
DOI : 10.1006/inco.1994.1003

URL : https://hal.archives-ouvertes.fr/inria-00075174

R. Crubillé and U. D. Lago, On Probabilistic Applicative Bisimulation and Call-by-Value ??-Calculi, Programming Languages and Systems -23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software Proceedings, pp.209-228, 2014.
DOI : 10.1007/978-3-642-54833-8_12

E. [. Dezani-ciancaglini and . Giovannetti, From B??hm's Theorem to Observational Equivalences, Electronic Notes in Theoretical Computer Science, vol.50, issue.2, pp.83-116, 2001.
DOI : 10.1016/S1571-0661(04)00167-7

[. Díaz-caro, S. Perdrix, C. Tasson, and B. Valiron, Equivalence of algebraic lambda-calculi -work in progress -. CoRR, abs, 1005.

M. Dezani-ciancaglini, J. Tiuryn, and P. Urzyczyn, Discrimination by Parallel Observers: The Algorithm, Information and Computation, vol.150, issue.2, pp.153-186, 1999.
DOI : 10.1006/inco.1998.2773

URL : http://doi.org/10.1006/inco.1998.2773

J. Desharnais, A. Edalat, and P. Panangaden, Bisimulation for Labelled Markov Processes, Information and Computation, vol.179, issue.2, pp.163-193, 2002.
DOI : 10.1006/inco.2001.2962

J. Desharnais, A. Edalat, and P. Panangaden, Bisimulation for Labelled Markov Processes, Information and Computation, vol.179, issue.2, pp.163-193, 2002.
DOI : 10.1006/inco.2001.2962

R. De, N. , and M. Hennessy, Testing equivalences for processes, Theor. Comput. Sci, vol.34, pp.83-133, 1984.

V. Danos and R. Harmer, Probabilistic game semantics

H. Vincent-danos, L. Herbelin, and . Regnier, Game semantics & abstract machines, Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, pp.394-405, 1996.

U. Dal, L. , and M. Zorzi, Probabilistic operational semantics for the lambda calculus. RAIRO -Theor, Inf. and Applic, vol.46, issue.3, pp.413-450, 2012.

A. Liguoro and . Piperno, Nondeterministic Extensions of Untyped ??-Calculus, Information and Computation, vol.122, issue.2, pp.149-177, 1995.
DOI : 10.1006/inco.1995.1145

V. Danos and L. Regnier, Head linear reduction, 2004.

[. Ehrhard, On Köthe sequence spaces and linear logic, Mathematical Structures in Computer Science, vol.12, issue.5, 2002.

[. Ehrhard, Finiteness spaces, Mathematical Structures in Computer Science, vol.15, issue.4, pp.615-646, 2005.
DOI : 10.1017/S0960129504004645

URL : https://hal.archives-ouvertes.fr/hal-00150276

T. Ehrhard, O. L. , T. Ehrhard, and O. Laurent, Acyclic solos and differential interaction nets Interpreting a finitary picalculus in differential interaction nets, Logical Methods in Computer Science Inf. Comput, vol.6, issue.2086, pp.606-633, 2010.

T. Ehrhard, M. Pagani, and C. Tasson, The Computational Meaning of Probabilistic Coherence Spaces, 2011 IEEE 26th Annual Symposium on Logic in Computer Science, pp.87-96, 2011.
DOI : 10.1109/LICS.2011.29

[. Ehrhard, M. Pagani, and C. Tasson, Probabilistic coherence spaces are fully abstract for probabilistic PCF, Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, 2014.
DOI : 10.1145/2535838.2535865

T. Ehrhard and L. Regnier, The differential lambdacalculus, Theor. Comput. Sci, vol.309, issue.1, 2003.
URL : https://hal.archives-ouvertes.fr/hal-00150572

T. Ehrhard and L. Regnier, B??hm Trees, Krivine???s Machine and the Taylor Expansion of Lambda-Terms, Lecture Notes in Computer Science, vol.227, issue.1???2, pp.186-197, 2006.
DOI : 10.1093/logcom/10.3.411

T. Ehrhard and L. Regnier, Differential interaction nets, Theoretical Computer Science, vol.364, issue.2, pp.166-195, 2006.
DOI : 10.1016/j.tcs.2006.08.003

URL : https://hal.archives-ouvertes.fr/hal-00150274

A. D. Gordon, M. Aizatulin, J. Borgström, G. Claret, T. Graepel et al., A model-learner pattern for bayesian reasoning, The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13, pp.403-416, 2013.

J. Chr, T. T. Godskesen, and . Hildebrandt, Extending Howe's method to early bisimulations for typed mobile embedded resources with local names, FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science, 25th International Conference Proceedings, pp.140-151, 2005.

J. Girard, Linear logic, Theoretical Computer Science, vol.50, issue.1, pp.1-102, 1987.
DOI : 10.1016/0304-3975(87)90045-4

URL : https://hal.archives-ouvertes.fr/inria-00075966

J. Girard, Normal functors, power series and lambda-calculus
DOI : 10.1016/0168-0072(88)90025-5

URL : http://doi.org/10.1016/0168-0072(88)90025-5

S. Goldwasser and S. Micali, Probabilistic encryption, Journal of Computer and System Sciences, vol.28, issue.2, pp.270-299, 1984.
DOI : 10.1016/0022-0000(84)90070-9

N. D. Goodman, The principles and practice of probabilistic programming, The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13, pp.399-402, 2013.

]. A. Gor98 and . Gordon, Operational equivalences for untyped and polymorphic object calculi, Higher Order Operational Techniques in Semantics, pp.9-54, 1998.

A. D. Gordon, Bisimilarity as a theory of functional programming, Theoretical Computer Science, vol.228, issue.1-2, pp.5-47, 1999.
DOI : 10.1016/S0304-3975(98)00353-3

M. Hennessy, Exploring probabilistic bisimulations, part I. Formal Asp, Comput, vol.24, issue.4-6, pp.749-768, 2012.

D. J. Howe, Proving Congruence of Bisimulation in Functional Programming Languages, Information and Computation, vol.124, issue.2, pp.103-112, 1996.
DOI : 10.1006/inco.1996.0008

G. [. Jones and . Plotkin, A probabilistic powerdomain of evaluations, [1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science, pp.186-195, 1989.
DOI : 10.1109/LICS.1989.39173

[. Jagadeesan and P. Panangaden, A domain-theoretic model for a higher-order process calculus, Automata, Languages and Programming, 17th International Colloquium Proceedings, pp.181-194, 1990.
DOI : 10.1007/BFb0032031

A. Jeffrey and J. Rathke, Towards a theory of bisimulation for local names, Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158), pp.56-66, 1999.
DOI : 10.1109/LICS.1999.782586

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.311-321, 2000.
DOI : 10.1109/LICS.2000.855780

[. Koutavas, P. B. Levy, and E. Sumii, From Applicative to Environmental Bisimulation, Electronic Notes in Theoretical Computer Science, vol.276, pp.215-235, 2011.
DOI : 10.1016/j.entcs.2011.09.023

J. Krivine, Lambda-calculus, types and models. Ellis Horwood series in computers and their applications, 1993.
URL : https://hal.archives-ouvertes.fr/cel-00574575

S. B. Lassen, Relational Reasoning about Functions and Nondeterminism, 1998.

J. Lévy, An algebraic interpretation of equality in some models of the lambda calculus, Lambda Calculus and Computer Science Theory, pp.147-165, 1975.

L. Paul-blain, Infinitary howe's method, Electr. Notes Theor. Comput. Sci, vol.164, issue.1, pp.85-104, 2006.

G. Longo, Set-theoretical models of ??-calculus: theories, expansions, isomorphisms, Annals of Pure and Applied Logic, vol.24, issue.2, pp.153-188, 1983.
DOI : 10.1016/0168-0072(83)90030-1

[. Larsen and A. Skou, Bisimulation through probabilistic testing, Information and Computation, vol.94, issue.1, pp.1-28, 1991.
DOI : 10.1016/0890-5401(91)90030-6

URL : http://doi.org/10.1016/0890-5401(91)90030-6

U. Dal-lago, D. Sangiorgi, and M. Alberti, On coinductive equivalences for higher-order probabilistic functional programs, Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, pp.297-308, 2014.
DOI : 10.1145/2535838.2535872

URL : https://hal.archives-ouvertes.fr/hal-01091573

[. Melliès, A factorisation theorem in rewriting theory, Category Theory and Computer Science, pp.49-68, 1997.
DOI : 10.1007/BFb0026981

[. Milner, Functions as processes, Mathematical Structures in Computer Science, vol.4, issue.02, pp.119-141, 1992.
DOI : 10.1016/0304-3975(87)90045-4

URL : https://hal.archives-ouvertes.fr/inria-00075405

[. Mascari and M. Pedicini, Head linear reduction and pure proof net extraction, Theoretical Computer Science, vol.135, issue.1, pp.111-137, 1994.
DOI : 10.1016/0304-3975(94)90263-1

URL : http://doi.org/10.1016/0304-3975(94)90263-1

]. Ong93 and . Ong, Non-determinism in a functional setting, [1993] Proceedings Eighth Annual IEEE Symposium on Logic in Computer Science, pp.19-23, 1993.
DOI : 10.1109/LICS.1993.287580

[. Panangaden, Probabilistic bisimulation, Advanced Topics in Bisimulation and Coinduction, pp.290-326, 2011.
DOI : 10.1017/CBO9780511792588.008

URL : https://hal.archives-ouvertes.fr/hal-00155306

S. Park, A calculus for probabilistic languages, Proceedings of the 2003 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, TLDI '03, pp.38-49, 2003.

A. Pfeffer and . Ibal, A probabilistic rational programming language, Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence, pp.733-740, 2001.

]. A. Pit97 and . Pitts, Operationally-based theories of program equivalence, Semantics and Logics of Computation, Publications of the Newton Institute, pp.241-298, 1997.

A. M. Pitts, Howe's method for higher-order languages, Advanced Topics in Bisimulation and Coinduction, pp.197-232, 2011.
DOI : 10.1017/CBO9780511792588.006

G. D. Plotkin, Call-by-name, call-by-value and the ??-calculus, Theoretical Computer Science, vol.1, issue.2, pp.125-159, 1975.
DOI : 10.1016/0304-3975(75)90017-1

[. Park, F. Pfenning, and S. Thrun, A probabilistic language based on sampling functions, ACM Transactions on Programming Languages and Systems, vol.31, issue.1, 2008.
DOI : 10.1145/1452044.1452048

M. Pagani and S. Rocca, Linearity, nondeterminism and solvability, Fundamenta Informaticae, vol.103, issue.1-4, pp.173-202, 2010.

M. Pagani and P. Tranquilli, Parallel Reduction in Resource Lambda-Calculus
DOI : 10.1007/978-3-642-10672-9_17

URL : https://hal.archives-ouvertes.fr/hal-00699013

R. Regnier, Une ??quivalence sur les lambda- termes, Programming Languages and Systems, 7th Asian Symposium Proceedings, pp.226-242281, 1994.
DOI : 10.1016/0304-3975(94)90012-4

[. Ramsey and A. Pfeffer, Stochastic lambda calculus and monads of probability distributions, Conference Record of POPL 2002: The 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.154-165, 2002.

D. Sangiorgi, The lazy lambda calculus in a concurrency scenario, [1992] Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science, pp.120-153, 1994.
DOI : 10.1109/LICS.1992.185524

D. Sangiorgi, Introduction to Bisimulation and Coinduction, 2011.
DOI : 10.1017/CBO9780511777110

URL : https://hal.archives-ouvertes.fr/hal-00907026

[. Selinger, Towards a quantum programming language, Mathematical Structures in Computer Science, vol.14, issue.4, pp.527-586, 2004.
DOI : 10.1017/S0960129504004256

D. Sangiorgi, N. Kobayashi, and E. Sumii, Logical Bisimulations and Functional Languages, International Symposium on Fundamentals of Software Engineering, International Symposium, FSEN 2007 Proceedings, pp.364-379, 2007.
DOI : 10.1007/978-3-540-75698-9_24

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.119.6202

D. Sangiorgi, N. Kobayashi, and E. Sumii, Environmental bisimulations for higher-order languages, ACM Trans. Program. Lang. Syst, vol.33, issue.1, p.5, 2011.
URL : https://hal.archives-ouvertes.fr/hal-01337665

[. Sumii and B. C. Pierce, A bisimulation for dynamic sealing, Theoretical Computer Science, vol.375, issue.1-3, pp.169-192, 2007.
DOI : 10.1016/j.tcs.2006.12.032

[. Sumii and B. C. Pierce, A bisimulation for type abstraction and recursion, J. ACM, vol.54, issue.5, 2007.

D. Sangiorgi and D. Walker, The pi-calculus ? a theory of mobile processes, 2001.

M. Takahashi, Parallel reductions in ?-calculus, Inf. Comput, vol.118, issue.1, 1995.

L. Vaux, On Linear Combinations of ??-Terms, Term Rewriting and Applications, 18th International Conference Proceedings, pp.374-388, 2007.
DOI : 10.1007/978-3-540-73449-9_28

URL : https://hal.archives-ouvertes.fr/hal-00383896

L. Vaux, The algebraic lambda calculus, Mathematical Structures in Computer Science, vol.12, issue.05, pp.1029-1059, 2009.
DOI : 10.1016/S0304-3975(03)00392-X

URL : https://hal.archives-ouvertes.fr/hal-00379750

M. W. Franck-van-breugel, J. Mislove, J. Ouaknine, and . Worrell, Domain theory, testing and simulation for labelled Markov processes, Theoretical Computer Science, vol.333, issue.1-2, pp.171-197, 2005.
DOI : 10.1016/j.tcs.2004.10.021