S. Abramsky, Research Topics in Functional Programming, pp.65-117, 1990.

S. Abramsky and A. Jung, Domain theory. In: Handbook of Logic in Computer Science, pp.1-168, 1994.

S. Abramsky and C. L. Ong, Full abstraction in the lazy lambda calculus, Inf. Comput, vol.105, issue.2, pp.159-267, 1993.

A. Appel and D. 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. 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.137, pp.39-55, 1970.

A. Bauer and M. Pretnar, Programming with algebraic effects and handlers, J. Log. Algebr. Meth. Program, vol.84, issue.1, pp.108-123, 2015.

N. Benton, A. Kennedy, L. Beringer, and M. Hofmann, Relational semantics for effect-based program transformations: higher-order store, Proc. of PPDP, pp.301-312, 2009.

D. Biernacki, S. Lenglet, and P. Polesiuk, Proving soundness of extensional normalform bisimilarities, Electr. Notes Theor. Comput. Sci, vol.336, pp.41-56, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01650000

A. Bizjak and L. Birkedal, Step-indexed logical relations for probability, Proc. of FOSSACS 2015, pp.279-294, 2015.

C. Böhm, Alcune proprietà delle forme ??-normali del ?k-calcolo. Pubblicazioni dell'Istituto per le Applicazioni del Calcolo, vol.696, 1968.

S. Burris and H. Sankappanavar, A course in universal algebra. Graduate texts in mathematics, 1981.

R. Crubillé and U. Dal-lago, On probabilistic applicative bisimulation and call-byvalue lambda-calculi, Proc. of ESOP, pp.209-228, 2014.

R. Culpepper and A. Cobb, Contextual equivalence for probabilistic programs with continuous random variables and scoring, Proceedings of ESOP 2017, pp.368-392, 2017.

U. Dal-lago, F. Gavazzo, and P. Levy, Effectful applicative bisimilarity: Monads, relators, and howe's method, Proc. of LICS 2017, pp.1-12, 2017.

U. Dal-lago, D. Sangiorgi, and M. Alberti, On coinductive equivalences for higherorder probabilistic functional programs, Proc. of POPL, pp.297-308, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01091573

U. Dal-lago 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.

B. Davey and H. Priestley, Introduction to lattices and order, 1990.

U. De-liguoro and A. Piperno, Non deterministic extensions of untyped lambdacalculus, Inf. Comput, vol.122, issue.2, pp.149-177, 1995.

A. Durier, D. Hirschkoff, and D. Sangiorgi, Eager functions as processes, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, pp.364-373, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01917255

M. Felleisen and R. Hieb, The revised report on the syntactic theories of sequential control and state, Theor. Comput. Sci, vol.103, issue.2, pp.235-271, 1992.

F. Gavazzo, Quantitative behavioural reasoning for higher-order effectful programs: Applicative distances, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, pp.452-461, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01926069

J. A. Goguen, J. W. Thatcher, E. G. Wagner, and J. B. Wright, Initial algebra semantics and continuous algebras, J. ACM, vol.24, issue.1, pp.68-95, 1977.

J. Goubault-larrecq, S. Lasota, and D. Nowak, Logical relations for monadic types, Mathematical Structures in Computer Science, vol.18, issue.6, pp.1169-1217, 2008.

D. Hofmann and G. Seal, Monoidal Topology. A Categorical Approach to Order, Metric, and Topology. No. 153 in Encyclopedia of Mathematics and its Applications, 2014.

J. Hughes and B. Jacobs, Simulations in coalgebra, Theor. Comput. Sci, vol.327, issue.1-2, pp.71-108, 2004.

M. Hyland, G. D. Plotkin, and J. Power, Combining effects: Sum and tensor, Theor. Comput. Sci, vol.357, issue.1-3, pp.70-99, 2006.

M. Hyland and J. Power, The category theoretic understanding of universal algebra: Lawvere theories and monads, Electr. Notes Theor. Comput. Sci, vol.172, pp.437-458, 2007.

P. Johann, A. Simpson, and J. Voigtländer, A generic operational metatheory for algebraic effects, Proc. of LICS 2010, pp.209-218, 2010.

C. Jones, Probabilistic non-determinism, 1990.

S. Katsumata and T. Sato, Foundations of Software Science and Computation Structures -16th International Conference, FOSSACS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, pp.145-160, 2013.

V. Koutavas, P. B. Levy, and E. Sumii, From applicative to environmental bisimulation, Electr. Notes Theor. Comput. Sci, vol.276, pp.215-235, 2011.

K. G. Larsen and A. Skou, Bisimulation through probabilistic testing, Proceedings of POPL 1989, pp.344-352, 1989.

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

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

S. B. Lassen, Bisimulation in untyped lambda calculus: Böhm trees and bisimulation up to context, Electr. Notes Theor. Comput. Sci, vol.20, pp.346-374, 1999.

S. B. Lassen, Eager normal form bisimulation, Proceedings of LICS 2005, pp.345-354, 2005.

S. B. Lassen, Normal form simulation for mccarthy's amb, Electr. Notes Theor. Comput. Sci, vol.155, pp.445-465, 2006.

W. F. Lawvere, Functorial Semantics of Algebraic Theories, 2004.

T. Leventis, Probabilistic böhm trees and probabilistic separation, Proc. of LICS, 2018.

J. Lévy, An algebraic interpretation of the lambda beta -calculus and a labeled lambda -calculus, Lambda-Calculus and Computer Science Theory, Proceedings of the Symposium Held in, pp.147-165, 1975.

P. Levy, Similarity quotients as final coalgebras, Proc. of FOSSACS 2011, vol.6604, pp.27-41, 2011.

P. Levy, J. Power, and H. Thielecke, Modelling environments in call-by-value programming languages, Inf. Comput, vol.185, issue.2, pp.182-210, 2003.

G. Longo, Set-theoretical models of lambda calculus: Theories, expansions, isomorphisms, Annals of Pure and Applied Logic, vol.24, pp.153-188, 1983.

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

I. A. Mason and C. L. Talcott, Equivalence in functional languages with effects, J. Funct. Program, vol.1, issue.3, pp.287-327, 1991.

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

E. Moggi, Computational lambda-calculus and monads, Proc. of LICS 1989, pp.14-23, 1989.

E. Moggi, Notions of computation and monads, Inf. Comput, vol.93, issue.1, pp.55-92, 1991.

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

C. L. Ong, Non-determinism in a functional setting, Proc. of LICS, pp.275-286, 1993.

C. Ong, The Lazy Lambda Calculus: An Investigation Into the Foundations of Functional Programming, 1988.

G. Plotkin, Call-by-name, call-by-value and the lambda-calculus, Theoretical Computer Science, vol.1, issue.2, pp.125-159, 1975.

G. Plotkin, Lambda-definability and logical relations, 1973.

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

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

G. D. Plotkin and J. Power, Algebraic operations and generic effects, Applied Categorical Structures, vol.11, issue.1, pp.69-94, 2003.

G. D. Plotkin and M. Pretnar, Handling algebraic effects, Logical Methods in Computer Science, vol.9, issue.4, 2013.

D. Pous and D. Sangiorgi, Enhancements of the bisimulation proof method, Advanced Topics in Bisimulation and Coinduction, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00909391

J. Reynolds, Types, abstraction and parametric polymorphism, IFIP Congress, pp.513-523, 1983.

D. Sands, Improvement theory and its applications, Higher Order Operational Techniques in Semantics, pp.275-306, 1998.

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

D. Sangiorgi, A theory of bisimulation for the pi-calculus, CONCUR '93, 4th International Conference on Concurrency Theory, pp.127-142, 1993.

D. Sangiorgi, The lazy lambda calculus in a concurrency scenario, Inf. Comput, vol.111, issue.1, pp.120-153, 1994.

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

A. Simpson and N. Voorneveld, Behavioural equivalence via modalities for algebraic effects, Proc. of ESOP, pp.300-326, 2018.

K. Støvring and S. B. Lassen, A complete, co-inductive syntactic theory of sequential control and state, Proceedings of POPL 2007, pp.161-172, 2007.

V. Strassen, The existence of probability measures with given marginals, Ann. Math. Statist, vol.36, issue.2, pp.423-439, 1965.

A. Tarski, A lattice-theoretical fixpoint theorem and its applications, Pacific J. Math, vol.5, issue.2, pp.285-309, 1955.

A. Thijs, Simulation and fixpoint semantics, Rijksuniversiteit Groningen, 1996.

C. Villani, Optimal Transport: Old and New. Grundlehren der mathematischen Wissenschaften, 2008.

P. Wadler, Proceedings of the NATO Advanced Study Institute on Program Design Calculi, Marktoberdorf, Program Design Calculi, pp.233-264, 1992.