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.

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

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 https://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

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

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

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

S. Maclane, Categories for the Working Mathematician, 1971.

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

A. M. Pitts, Operationally-Based Theories of Program Equivalence, Semantics and Logics of Computation, Publications of the Newton Institute, pp.241-298, 1997.
DOI : 10.1017/CBO9780511526619.007
URL : http://www.cs.tau.ac.il/~nachumd/formal/exam/pitts.pdf

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, Algebraic operations and generic effects, Applied Categorical Structures, vol.11, issue.1, pp.69-94, 2003.