C. Lago, We start by de ning the notion of Howe's extension, a construction extending a ?-term V-open relation to a compatible and substitutive ?-term V-relation. 2. For any a ? V if ?, x : s ? |= v a ? ? H (u, z) : ? is derivable, 2015.

, The proof is by induction on the derivation of the judgments: J ?, x : s ? |= ? a ? ? H (e, f ) : ? J ?

. H-var, x : s ? v ? (x, u) : ? ?, x : s ? |= v a ? ? H (x, u) : ? (H-var), so that s ? 1 and J is ?, x : s ? |= v a ? ? H (x, u) : ? . We have to prove a ?s ? ( v ? H ( , w )) ? ? v ? H ( , u[w/x]) : ? . Since ? is value substitutive, from ?, x : s ? |= v a ? ? H (x, u) : ? we infer a ? ? v ? (w, u[w/x]) : ? . Moreover, since ? H is an open ?-term V-relation (and thus closed under weakening), We have two subcases to consider. 1.1 J has been inferred via an instance of rule (H-var) from premises: a ? ?

H. ?-?-v-?,

, 2 J has been inferred via an instance of rule (H-var) from premises: a ? ?, : r ?

, u) : ? . We have to prove a ? s ? (? v ? H ( , w )) ? ?, : r ? v ? H ( , u[w/x]) : ? . As V is integral and ? is value-substitutive, we have: a ? s ? (? v ? H ( , w )) ? a ? ?, J is ?

, Suppose J has been inferred via an instance of rule (H-let) from premises: ?, x : s ? |= ? a ? ? H (e, e ) : ? (12.1)

?. ,

, x : s ? ) ? (?, x : r ? ) ? H (let = e in f , ) : ? . (12.3) so that is: (p ? 1) · ? ? ?, x : (p?1) ·s ?r ? |= ? (p ? 1)(a) ? b ? c ? ? H

, First of all we observe that since ? H is re exive, we can assume n = m. In fact, if e.g. n = m + l, then we can 'complete' (? H ) (m) as follows: (? H ) (m) = (? H ) (m) ·I · · · · I l -times ? (? H ) (m) · ? H · · · · ? H l -times = (? H ) (n)

, The base case is trivial. Let us turn on the inductive step. We have to prove: (s ? 1) ? e (? ? H (e, e ) : ? ) ? (? (? H ) (n) (e , e ) : ? ) ? f (?, x : s ? ? H ( f , f ) : ? ) ? (?, x : s ? (? H ) (n) ( f , f ) : ? ) ? c

, ) : ? ) ? (?, x : s ? (? H ) (n) ( f , f ) : ? ) ? c, i.e. (s ? 1) ? (? ? H (e, e ) : ? ) ? (?, x : s ? ? H ( f , f ) : ? ) ? (s ? 1) ? (? (? H

. ?-(?, x : s ? (? H ) (n) ( f , f ) : ? ) ? c

, We can now apply compatibility of ? H plus the induction hypothesis, thus reducing the thesis to: (s ? 1) · ? ? ? ? H (let x = e in f

, ? (s ? 1) · ? ? ? (? H ) T (let x = e in f , let x = e in f ) : ? ) ? c

, We can now conclude the thesis by very de nition of (? H ) T . To prove point 2 we have to show (? H ) T ? ((? H ) T ) ? . For that it is su cient to show ? H ? ((? H ) T ) ? . That amounts to prove that for all computations ? e, e : ? and values ? v , and for any a ? V such that ? |= ? a ? ? H (e, e ) : ? is derivable we have a ? ? (? H ) T (e, e ) : ? (and similarity for ? v , : ? ). The proof is by induction on the derivation of ? |= ? a ? ? H

, If any CBE in ? is nitely continuous, Theorem 17

. T-=-?, One inequality follows from Lemma 41 as follows: ? ? ? H ? (? ) T . For the other inequality, we rely on the coinduction proof principle associated with ? , meaning that it is su cient to prove that ((? ) H ) T is a symmetric applicative simulation (with respect to ?). Symmetry is given by Lemma 45. From Lemma 43 (Key Lemma) we know that ? H is an applicative simulation distance. Since the identity ?-term V-relation is an applicative simulation distance, and the composition of applicative simulation distances is itself an applicative simulation distance (see Proposition 30), Lemma 45 we know that (? H ) T is compatible. Therefore, it is su cient to prove

, We conclude this chapter by noticing that we can rely on Theorem 17 to come up with concrete notions of compatible applicative bisimilarity distance. For instance, we obtain a compatible pseudometric for for P-Fuzz (observe that CBEs are indeed nitely continuous)

. Koutavas, normal form bisimilarity has been mainly investigated for call-by-name languages, due to its equivalence with Lévy-Longo tree equivalence, and for the so-called classical theory of ?-calculus (Barendregt, 1984), due to its equivalence with Böhm tree equivalence. To the best of the author's knowledge, no abstract account of normal form bisimilarity in the context of languages with algebraic e ects has been given so far. However, there are some works on speci c e ectful extensions of Böhm trees, notably the work of de Liguoro and Piperno on nondeterministic Böhm trees, de ned are proved using our abstract Howe's method. Applicative bisimilarity has also been investigated for languages with non-algebraic e ects, notably for languages with control operators (Biernacki & Lenglet, 1993.

, Similar in spirit to our approach, the work of Katsumata and Sato (Katsumata & Sato, 2013) (as well as (Katsumata, 2013)) analyses monadic lifting of relations in the context of -lifting

. Simpson, . Voigtländer-(johann, . Simpson, and . Voigtländer, Concerning program metrics, several works have been done in the past years on quantitative reasoning in the context of programming language semantics. In particular, several authors have used (cartesian) categories of ultrametric spaces as a foundation for denotational semantics of both concurrent, Another piece of work which is related to ours is due to Johann, 1980.

D. Du, . Gebler, K. G. Gebler, and . Tini-;-de-amorim, 2017) is a denotational version of the so-called metric preservation (Reed & Pierce, 2010) (whose original proof requires a suitable step-indexed metric logical relation). Corollary 6 is the operational counterpart of such result generalised to arbitrary algebraic e ects. A di erent but deeply related line of research has been recently proposed in, where coinductive, operationally-based distances have been studied for probabilistic ?-References Abramsky, pp.65-117, 1990.

S. Abramsky, Research topics in functional programming, pp.65-116, 1990.

S. Abramsky and A. Jung, Domain theory, 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.

A. Arnold and M. Nivat, Metric interpretations of in nite trees and semantics of non deterministic recursive programs, Theor. Comput. Sci, vol.11, pp.181-205, 1980.

J. W. Backus, F. L. Bauer, J. Green, C. Katz, J. Mccarthy et al., Report on the algorithmic language algol 60, Commun. ACM, vol.3, issue.5, pp.299-314, 1960.

P. Baldan, F. Bonchi, H. Kerstan, and B. König, Behavioral metrics via functor lifting, Proc. of FSTTCS, pp.403-415, 2014.

P. Baldan, F. Bonchi, H. Kerstan, and B. König, Towards trace metrics via functor lifting, Proc. of CALCO 2015, pp.35-49, 2015.

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

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

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

N. Benton, J. Hughes, and E. Moggi, Monads and e ects, Applied semantics, international summer school, APPSEM, advanced lectures, pp.42-122, 2000.

D. Biernacki and S. Lenglet, Applicative bisimilarities for call-by-name and call-by-value ?µcalculus, Electr. Notes Theor. Comput. Sci, vol.308, pp.49-64, 2014.

D. Biernacki, S. Lenglet, and P. Polesiuk, Proving soundness of extensional normal-form bisimilarities, Electr. Notes Theor. Comput. Sci, vol.336, pp.41-56, 2018.

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.

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

J. I. Brachthäuser and P. Schuster, E ekt: Extensible algebraic e ects in scala (short paper), Proceedings of the 8th acm sigplan international symposium on scala, pp.67-72, 2017.

A. Brunel, M. Gaboardi, D. Mazza, and S. Zdancewic, A core quantitative coe ect calculus, Proc. of ESOP, pp.351-370, 2014.

R. Bruni and F. Gadducci, Some algebraic laws for spans (and their connections with multirelations), Electronic Notes in Theoretical Computer Science, vol.44, issue.3, pp.175-193, 2001.

A. Carboni, S. Kasangian, and R. Street, Bicategories of spans and relations, Journal of Pure and Applied Algebra, vol.33, issue.3, pp.259-267, 1984.

A. Carraro and G. Guerrieri, A semantical and operational account of call-by-value solvability, Foundations of software science and computation structures -17th international conference, FOSSACS 2014, held as part of the european joint conferences on theory and practice of software, pp.103-118, 2014.

A. Church, The calculi of lambda conversion. (am-6) (annals of mathematics studies), 1985.

P. Clément and W. Desch, Wasserstein metric and subordination, vol.189, 2008.

M. Clementino and W. Tholen, From lax monad extensions to topological theories, vol.46, pp.99-123, 2014.

R. Crubillé and U. Lago, On probabilistic applicative bisimulation and call-by-value lambdacalculi, Proc. of ESOP, pp.209-228, 2014.

R. Crubillé and U. Lago, Metric reasoning about lambda-terms: The a ne case, Proc. of LICS, pp.633-644, 2015.

R. Crubillé and U. Lago, Metric reasoning about lambda-terms: The general case, Proc. of ESOP 2017, pp.341-367, 2017.

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, D. Sangiorgi, and M. Alberti, On coinductive equivalences for higher-order probabilistic functional programs, Proc. of POPL, pp.297-308, 2014.

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.

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

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.

J. De-bakker and J. Zucker, Denotational semantics of concurrency, Stoc, pp.153-158, 1982.

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

F. De-saussure and W. Baskin, Course in general linguistics: Translated by wade baskin. edited by perry meisel and haun saussy, 2011.

E. P. De-vink and J. J. Rutten, Bisimulation for probabilistic transition systems: A coalgebraic approach, Automata, languages and programming, 24th international colloquium, icalp'97, pp.460-470, 1997.

S. Dolan, S. Eliopoulos, D. Hillerström, A. Madhavapeddy, K. C. Sivaramakrishnan et al., Concurrent system programming with e ect handlers, Trends in functional programming -18th international symposium, pp.98-117, 2017.

D. Donkel, The theory of di erence: Readings in contemporary continental thought. State University of, 2001.

W. Du, Y. Deng, and D. Gebler, Behavioural pseudometrics for nondeterministic probabilistic systems, Proc. of SETTA 2016, pp.67-84, 2016.

A. Durier, D. Hirschko, 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.

C. Dwork, Di erential privacy, Automata, languages and programming, pp.1-12, 2006.

M. Escardo, A metric model of pcf, Workshop on realizability semantics and applications, 1999.

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.

M. Gabbrielli, S. Martini, . Springer, M. Gaboardi, S. Katsumata et al., Programming languages: Principles and paradigms, Proc. of ICFP 2016, pp.476-489, 2010.

D. Gebler, K. G. , L. Tini, and S. , Compositional bisimulation metric reasoning with probabilistic process calculi, Logical Methods in Computer Science, vol.12, issue.4, 2016.

J. Girard, A. Scedrov, and P. Scott, Bounded linear logic: A modular approach to polynomial-time computability, Theor. Comput. Sci, vol.97, pp.1-66, 1992.

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.

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.

I. Hasuo, B. Jacobs, and A. Sokolova, Generic trace semantics via coinduction, Logical Methods in Computer Science, vol.3, issue.4, 2007.

F. Hausdor, Grundzüge der mengenlehre, 1949.

C. Hermida and B. Jacobs, Structural induction and coinduction in a brational setting, Inf. Comput, vol.145, issue.2, pp.107-152, 1998.

D. Ho-man, A cottage industry of lax extensions. Categories and General Algebraic Structures with Applications, vol.3, pp.113-151, 2015.

D. Hofmann, Topological theories and closed objects, Adv. Math, vol.215, pp.789-824, 2007.

D. Hofmann and C. Reis, Convergence and quantale-enriched categories. Categories and General Algebraic Structures with Applications, vol.9, pp.77-138, 2018.

D. Hofmann and G. Seal, Monoidal topology. a categorical approach to order, metric, and topology, 2014.

R. Howard, Dynamic probabilistic systems, 2007.

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.

M. Hyland, P. B. Levy, G. D. Plotkin, and J. Power, Combining algebraic e ects with continuations, Theor. Comput. Sci, vol.375, issue.1-3, pp.20-40, 2007.

M. Hyland, G. D. Plotkin, and J. Power, Combining e ects: 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.

B. Jacobs, Introduction to coalgebra: Towards mathematics of states and observation, vol.59, 2016.

B. Jacobs, A. Silva, and A. Sokolova, Trace semantics via determinization, Coalgebraic methods in computer science -11th international workshop, vol.2012, pp.109-129, 2012.

T. Jech, Set theory, 1997.

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

S. Katsumata, Relating computational e ects by -lifting, Inf. Comput, vol.222, pp.228-246, 2013.

S. Katsumata and T. Sato, Preorders on monads and coalgebraic simulations, 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, pp.145-160, 2013.

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

A. Kock, Strong functors and monoidal monads, Archiv der Mathematik, issue.23, pp.113-120, 1972.

K. Kortanek and M. Yamasaki, Discrete in nite transportation problems, Discrete Applied Mathematics, issue.58, pp.19-33, 1995.

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

A. Kurz and J. Velebil, Relation lifting, a survey, J. Log. Algebr. Meth. Program, vol.85, issue.4, pp.475-499, 2016.

P. Landin, Correspondence between ALGOL 60 and church's lambda-notation: part I, Commun. ACM, vol.8, issue.2, pp.89-101, 1965.

P. Landin, A correspondence between ALGOL 60 and church's lambda-notations: Part II, Commun. ACM, vol.8, issue.3, pp.158-167, 1965.

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 (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, Eager normal form bisimulation, Proceedings of LICS 2005, pp.345-354, 2005.

S. B. Lassen, Head normal form bisimulation for pairs and the \lambda\mu-calculus, Proceedings of LICS, pp.297-306, 2006.

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

F. Lawvere, Metric spaces, generalized logic, and closed categories, Rend. Sem. Mat. Fis. Milano, vol.43, pp.135-166, 1973.

W. F. Lawvere, Functorial Semantics of Algebraic Theories. Reprints in Theory and Applications of Categories, vol.4, pp.1-121, 2004.

D. Leijen, Implementing algebraic e ects in c, Programming languages and systems, pp.339-363, 2017.

T. Leventis, Probabilistic lambda-theories (Unpublished doctoral dissertation), 2016.

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, pp.147-165, 1975.

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.

P. B. Levy, Amb breaks well-pointedness, ground amb doesn't. Electronic Notes in Theoretical Computer Science, Proceedings of the 23rd Conference on the Mathematical Foundations of Programming Semantics, vol.173, pp.221-239, 2007.

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

A. Lopez and A. Simpson, Basic operational preorders for algebraic e ects in general, and for combined probability and nondeterminism in particular, 27th EACSL annual conference on computer science logic, CSL 2018, vol.29, pp.1-29, 2018.

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

E. Manes, A triple theoretic construction of compact algebras, Seminar on triples and categorical homology theory, pp.91-118, 1969.

E. G. Manes, Taut monads and t0-spaces, Theor. Comput. Sci, vol.275, issue.1-2, pp.79-109, 2002.

J. Maraist, M. Odersky, D. Turner, and P. Wadler, Call-by-name, call-by-value, call-by-need and the linear lambda calculus, Theor. Comput. Sci, vol.228, issue.1-2, pp.175-210, 1999.

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.

C. Mclaughlin, J. Mckinna, and I. Stark, Triangulating context lemmas, Proceedings of the 7th acm sigplan international conference on certi ed programs and proofs, pp.102-114, 2018.

R. Milner, Fully abstract models of typed lambda-calculi, Theor. Comput. Sci, vol.4, issue.1, pp.1-22, 1977.

R. Milner, Communication and concurrency, 1989.

R. Milner, Functions as processes, Mathematical Structures in Computer Science, vol.2, issue.2, pp.119-141, 1992.

R. Milner and M. Tofte, Co-induction in relational semantics, Theor. Comput. Sci, vol.87, issue.1, pp.209-220, 1991.

R. Milner, M. Tofte, and R. Harper, De nition of standard ML, 1990.

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 (Unpublished doctoral dissertation), 1969.

J. Munkres, , 2000.

C. Ong, The lazy lambda calculus: An investigation into the foundations of functional programming, 1988.

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

D. Park, Concurrency and automata on in nite sequences, Theoretical computer science, pp.167-183, 1981.

T. Petricek, D. A. Orchard, and A. Mycroft, Coe ects: a calculus of context-dependent computation, Proc. of ICFP, pp.123-135, 2014.

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. Plotkin, Call-by-name, call-by-value and the lambda-calculus, Theoretical Computer Science, vol.1, issue.2, pp.125-159, 1975.

G. Plotkin, Lcf considered as a programming language, Theoretical Computer Science, vol.5, issue.3, pp.223-255, 1977.

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.

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

G. D. Plotkin and M. Pretnar, Handling algebraic e ects, 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.

M. Pretnar, An introduction to algebraic e ects and handlers, Electr. Notes Theor. Comput. Sci, vol.319, pp.19-35, 2015.

M. O. Rabin and D. S. Scott, Finite automata and their decision problems, IBM Journal of Research and Development, vol.3, issue.2, pp.114-125, 1959.

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.

K. Rosenthal, Quantales and their applications, Longman Scienti c & Technical, 1990.

J. Rutten, Elements of generalized ultrametric domain theory, Theor. Comput. Sci, vol.170, issue.1-2, pp.349-381, 1996.

J. J. Rutten, Universal coalgebra: a theory of systems, Theor. Comput. Sci, vol.249, issue.1, pp.3-80, 2000.

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

D. Sangiorgi, The lazy lambda calculus in a concurrency scenario (extended abstract), Proceedings of the seventh annual symposium on logic in computer science (LICS '92), pp.102-109, 1992.

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, Introduction to bisimulation and coinduction, 2011.

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.

D. Sangiorgi and V. Vignudelli, Environmental bisimulations for probabilistic higher-order languages, Proceedings of POPL 2016, pp.595-607, 2016.

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

A. Schrijver, Theory of linear and integer programming, 1986.

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.

L. Steen and J. Seebach, Counterexamples in topology, 1995.

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.

C. Strachey, Fundamental concepts in programming languages. Higher-Order and Symbolic Computation, vol.13, pp.11-49, 2000.

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 xpoint theorem and its applications, Paci c J. Math, vol.5, issue.2, pp.285-309, 1955.

A. Thijs, Simulation and xpoint semantics, 1996.

A. M. Turing, Computability and ?-de nability, The Journal of Symbolic Logic, vol.2, issue.4, pp.153-163, 1937.

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.

W. Van-orman-quine, Word and object, 1964.

S. Vickers, Topology via logic, 1996.

C. Villani, Optimal transport: Old and new, 2008.

L. Xu, K. Chatzikokolakis, and H. Lin, Metrics for di erential privacy in concurrent systems, Formal techniques for distributed objects, components, and systems -34th IFIP WG 6.1 international conference, pp.199-215, 2014.