S. Abramsky, The lazy lambda calculus, Research Topics in Functional Programming, pp.65-117, 1990.

W. Andrew, D. A. Appel, and . Mcallester, An indexed model of recursive types for foundational proof-carrying code, ACM Trans. Program. Lang. Syst, vol.23, issue.5, pp.657-683, 2001.

H. P. Barendregt, The lambda calculus: its syntax and semantics. Studies in logic and the foundations of mathematics, 1984.

M. Barr, Relational algebras, Lect. Notes Math, vol.47, pp.39-55, 1970.
DOI : 10.1073/pnas.47.7.1043

N. Benton, A. Kennedy, L. Beringer, and M. Hofmann, Relational semantics for effect-based program transformations, Proceedings of the 11th ACM SIGPLAN conference on Principles and practice of declarative programming, PPDP '09, pp.301-312, 2009.
DOI : 10.1145/1599410.1599447

A. Bizjak and L. Birkedal, Step-Indexed Logical Relations for Probability, Proc. of FOSSACS 2015, pp.279-294, 2015.
DOI : 10.1007/978-3-662-46678-0_18

L. Roy, A. D. Crole, and . Gordon, Relating operational and denotational semantics for input/output effects, Mathematical Structures in Computer Science, vol.9, issue.2, pp.125-158, 1999.

R. Crubillé and U. D. Lago, On Probabilistic Applicative Bisimulation and Call-by-Value ??-Calculi, Proc. of ESOP 2014, pp.209-228, 2014.
DOI : 10.1007/978-3-642-54833-8_12

U. Dal-lago, F. Gavazzo, and P. Levy, Effectful applicative bisimilarity: Monads, relators, and Howe's method (long version) Available at http://arxiv, 2017.

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

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.

V. Danos and R. Harmer, Probabilistic game semantics, ACM Transactions on Computational Logic, vol.3, issue.3, pp.359-382, 2002.
DOI : 10.1145/507382.507385

A. Brian, H. A. Davey, and . Priestley, Introduction to lattices and order, 1990.

A. Ugo-de-'liguoro and . Piperno, Non deterministic extensions of untyped lambda-calculus, Inf. Comput, vol.122, issue.2, pp.149-177, 1995.

J. A. Goguen, J. W. Thatcher, E. G. Wagner, and J. B. Wright, Initial Algebra Semantics and Continuous Algebras, Journal of the ACM, vol.24, issue.1, pp.68-95, 1977.
DOI : 10.1145/321992.321997

S. Goncharov and L. Schröder, A Relatively Complete Generic Hoare Logic for Order-Enriched Effects, 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science, pp.273-282, 2013.
DOI : 10.1109/LICS.2013.33

A. D. Gordon, A Tutorial on Co-induction and Functional Programming, Workshops in Computing, pp.78-95, 1994.
DOI : 10.1007/978-1-4471-3573-9_6

J. Goubault-larrecq, S. Lasota, and D. Nowak, Logical relations for monadic types, Mathematical Structures in Computer Science, vol.1581, issue.06, pp.1169-1217, 2008.
DOI : 10.1006/inco.1996.0052

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

P. Johann, A. Simpson, and J. Voigtländer, A Generic Operational Metatheory for Algebraic Effects, 2010 25th Annual IEEE Symposium on Logic in Computer Science, pp.209-218, 2010.
DOI : 10.1109/LICS.2010.29

C. Jones, Probabilistic Non-determinism, 1990.

V. 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

B. Søren and . Lassen, Relational reasoning about contexts, Higher Order Operational Techniques in Semantics, pp.91-136, 1998.

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

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

L. Paul-blain, Similarity quotients as final coalgebras, Proc. of FOSSACS 2011, pp.27-41, 2011.

J. Paul-blain-levy, H. Power, and . Thielecke, Modelling environments in call-by-value programming languages, Information and Computation, vol.185, issue.2, pp.182-210, 2003.
DOI : 10.1016/S0890-5401(03)00088-9

E. Moggi, Computational lambda-calculus and monads, [1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science, pp.14-23, 1989.
DOI : 10.1109/LICS.1989.39155

J. Morris, Lambda Calculus Models of Programming Languages, 1969.

C. 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

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

D. Gordon, J. Plotkin, and . Power, Adequacy for algebraic effects, Proc. of FOSSACS 2001, pp.1-24, 2001.

D. Gordon, J. Plotkin, and . Power, Notions of computation determine monads, Proc. of FOSSACS 2002, pp.342-356, 2002.

J. J. Rutten, Universal coalgebra: a theory of systems, Theoretical Computer Science, vol.249, issue.1, pp.3-80, 2000.
DOI : 10.1016/S0304-3975(00)00056-6

D. Sangiorgi and V. Vignudelli, Environmental bisimulations for probabilistic higher-order languages, Proc. of POPL 2016, pp.595-607, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01337665

A. Schrijver, Theory of Linear and Integer Programming, 1986.

A. Marchienus and T. , Simulation and fixpoint semantics, Rijksuniversiteit Groningen, 1996.

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