S. Abramsky, The lazy lambda calculus, Research topics in functional programming, pp.65-117, 1990.

S. Abramsky and A. Jung, Domain theory, Handbook of logic in computer science, pp.1-168, 1994.

H. Barendregt, The lambda calculus: its syntax and semantics, 1984.

M. Barr, Relational algebras, Lect. Notes Math, vol.137, pp.39-55, 1970.

D. Biernacki, M. Piróg, P. Polesiuk, and F. Sieczkowski, Handle with care: relational interpretation of algebraic e ects and handlers. PACMPL, 2(POPL), vol.8, p.30, 2018.

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

R. Blute, J. Desharnais, A. Edalat, and P. Panangaden, Bisimulation for labelled markov processes, Proc. of LICS, pp.149-158, 1997.

J. Borgström, U. D. Lago, A. D. Gordon, and M. Szymczak, A lambda-calculus foundation for universal probabilistic programming, Proceedings of the 21st ACM SIGPLAN international conference on functional programming, pp.33-46, 2016.

R. Crubillé and U. Lago, On probabilistic applicative bisimulation and call-by-value 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, E ectful 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 higher-order probabilistic functional programs, Proc. of POPL, pp.297-308, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01091573

R. De-nicola and M. Hennessy, Testing equivalence for processes, Automata, languages and programming, 10th colloquium, pp.548-560, 1983.

A. De-amorim, M. Gaboardi, J. Hsu, S. Katsumata, and I. Cherigui, A semantic account of metric preservation, Proc. of POPL 2017, pp.545-556, 2017.

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

T. Ehrhard, M. Pagani, and C. Tasson, Measurable cones and stable, measurable functions: a model for probabilistic higher-order programming, PACMPL, 2(POPL), vol.59, p.28, 2018.
URL : https://hal.archives-ouvertes.fr/hal-02346093

F. Gavazzo, Quantitative behavioural reasoning for higher-order e ectful programs: Applicative distances, Proceedings of the 33rd annual ACM/IEEE symposium on logic in computer science, LICS 2018, pp.452-461, 2018.

M. Giry, A categorical approach to probability theory, Categorical aspects of topology and analysis, pp.68-85, 1982.

A. Gordon, A tutorial on co-induction and functional programming, Workshops in computing, pp.78-95, 1994.

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. Howe, Proving congruence of bisimulation in functional programming languages, Inf. Comput, vol.124, issue.2, pp.103-112, 1996.

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

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

C. Jones, Probabilistic non-determinism (Unpublished doctoral dissertation), 1990.

S. Katsumata, T. Sato, and T. Uustalu, Codensity lifting of monads and its dual, Logical Methods in Computer Science, vol.14, issue.4, 2018.

G. M. Kelly, Basic concepts of enriched category theory, Reprints in Theory and Applications of Categories, pp.1-136, 2005.

U. D. Lago and F. Gavazzo, E ectful normal form bisimulation, Proc. of ESOP, 2019.

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

S. Lassen, Relational reasoning about functions and nondeterminism (Unpublished doctoral dissertation), 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 and P. B. Levy, Typed normal form bisimulation, Computer science logic, 21st international workshop, pp.283-297, 2007.

P. Levy, In nitary howe's method, Electr. Notes Theor. Comput. Sci, vol.164, issue.1, pp.85-104, 2006.

P. Levy, Similarity quotients as nal 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.

S. Maclane, Categories for the working mathematician, 1971.

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

J. Morris, Lambda calculus models of programming languages (Unpublished doctoral dissertation), 1969.

P. Panangaden, The category of markov kernels, Electr. Notes Theor. Comput. Sci, vol.22, pp.171-187, 1999.

P. Panangaden, Probabilistic bisimulation, Advanced topics in bisimulation and coinduction, pp.290-326, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00155306

S. Park, F. Pfenning, and S. Thrun, A probabilistic language based upon sampling functions, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on principles of programming languages, pp.171-182, 2005.

A. Pitts, Howe's method for higher-order languages, Advanced topics in bisimulation and coinduction, vol.52, pp.197-232, 2011.

G. Plotkin, Lambda-de nability and logical relations, 1973.

G. D. Plotkin and J. Power, Adequacy for algebraic e ects, 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.

D. Pollard, R. Gill, and B. Ripley, A user's guide to measure theoretic probability, 2002.

N. Ramsey and A. Pfe-er, Stochastic lambda calculus and monads of probability distributions, Proc. of POPL, pp.154-165, 2002.

J. Reed and B. Pierce, Distance makes the types grow stronger: a calculus for di erential privacy, Proc. of ICFP 2010, pp.157-168, 2010.

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

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

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

T. Sato, Approximate relational hoare logic for continuous random samplings, Electr. Notes Theor. Comput. Sci, vol.325, pp.277-298, 2016.

D. Scott, Outline of a mathematical theory of computation, 1970.

D. Scott and C. Strachey, Toward a mathematical semantics for computer languages, 1971.

K. Sieber, Reasoning about sequential functions via logical relations, Applications of categories in computer science, vol.177, pp.258-269, 1992.

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

S. Staton, Commutative semantics for probabilistic programming, Programming languages and systems -26th european symposium on programming, pp.855-879, 2017.

S. Staton, H. Yang, F. D. Wood, C. Heunen, and O. Kammar, Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints, Proceedings of the 31st annual ACM/IEEE symposium on logic in computer science, LICS '16, pp.525-534, 2016.

A. Thijs, Simulation and xpoint semantics, 1996.

M. Vákár, O. Kammar, and S. Staton, A domain theory for statistical probabilistic programming, PACMPL, 3(POPL), vol.36, p.29, 2019.

F. Van-breugel, M. Mislove, J. Ouaknine, and J. Worrell, Domain theory, testing and simulation for labelled markov processes, Theor. Comput. Sci, vol.333, issue.1-2, pp.171-197, 2005.

M. Wand, R. Culpepper, T. Giannakopoulos, and A. Cobb, Contextual equivalence for a probabilistic language with continuous random variables and recursion. PACMPL, 2(ICFP), vol.87, p.30, 2018.