A. Aristizábal, D. Biernacki, S. Lenglet, and P. Polesiuk, Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt Generation Observational Equivalence as a Testing Equivalence, Proc. FSCD'16, pp.1-9, 1987.

]. S. Abr90 and . Abramsky, The Lazy Lambda Calculus In: Research topics in functional programming, pp.65-116, 1990.

]. P. Acz88 and . Aczel, Non-Well-Founded Sets, CSLI Lecture Notes. Stanford: CSLI, 1988.

A. [. Abadi and . Gordon, A bisimulation method for cryptographic protocols, Preliminary version appeared in Proc. ESOP'98, pp.267-303, 1998.
DOI : 10.1007/BFb0053560

C. [. Abramsky and . Ong, Full Abstraction in the Lazy Lambda Calculus, Information and Computation 105, pp.159-267, 1993.
DOI : 10.1006/inco.1993.1044

]. C. Bai98 and . Baier, On Algorithmic Verification Methods for Probabilistic Systems, 1998.

]. F. Bar02 and . Bartels, GSOS for Probabilistic Transition Systems, Proc. CMCS '02, pp.29-53, 2002.

]. H. Bar84 and . Barendregt, The Lambda Calculus: Its Syntax and Semantics, Studies in Logic and the Foundations of Mathematics 103, 1984.

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

U. [. Borgström, A. Dal-lago, M. Gordon, and . Szymczak, A lambdacalculus foundation for universal probabilistic programming, Proc. ICFP'16. 2016, pp.33-46

R. [. Bernardo, M. De-nicola, and . Loreti, A Companion of Relating Strong Behavioral Equivalences for Processes with Nondeterminism and Probabilitie, CoRR abs/1305, p.538, 2013.

]. M. Bdl14a, R. Bernardo, M. De-nicola, and . Loreti, Relating Strong Behavioral Equivalences for Processes with Nondeterminism and Probabilities, In: Theoretical Computer Science, 2014.

M. Bernardo, R. De-nicola, and M. Loreti, Revisiting Trace and Testing Equivalences for Nondeterministic and Probabilistic Processes, In: Logical Methods in Computer Science, vol.10, issue.1, pp.16-17, 2014.
DOI : 10.1007/978-3-642-28729-9_13

R. [. Boreale, R. De-nicola, and . Pugliese, Basic Observables for Processes, In: Information and Computation, vol.1491, pp.77-98, 1999.
DOI : 10.1006/inco.1998.2755
URL : https://doi.org/10.1006/inco.1998.2755

]. J. Ben83, . S. Benthem-[-bhr84-], C. Brookes, A. Hoare, and . Roscoe, Modal Logic and Classical Logic Napoli: Bibliopolis A Theory of Communicating Sequential Processes, Journal of the ACM, pp.31-560, 1983.

B. Bloom, S. Istrail, and A. Meyer, Bisimulation can't be traced, Journal of the ACM, vol.42, issue.1, pp.232-268, 1995.
DOI : 10.1145/200836.200876

]. A. Biz16 and . Bizjak, On Semantics and Applications of Guarded Recursion, 2016.

M. [. Baier and . Kwiatkowska, Domain equations for probabilistic processes, Mathematical Structures in Computer Science, vol.10, issue.6, pp.665-717, 2000.
DOI : 10.1017/S0960129599002984

D. Biernacki and S. Lenglet, Environmental Bisimulations for Delimited-Control Operators, Proc. APLAS'13, pp.333-348, 2013.
DOI : 10.1007/978-3-319-03542-0_24
URL : https://hal.archives-ouvertes.fr/hal-00862189

M. [. Bernardo and . Miculan, Disjunctive Probabilistic Modal Logic is Enough for Bisimilarity on Reactive Probabilistic Systems, Proc. ICTCS'16. 2016, pp.203-220

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

M. Boreale, D. Sangiorgi, M. Bernardo, D. Sangiorgi, and V. Vignudelli, Bisimulation in name-passing calculi without matching On the Discriminating Power of Passivation and Higher-Order Interaction, Proc. LICS'98 Proc. CSL-LICS'14, 1998.

]. M. Bsv14b, D. Bernardo, V. Sangiorgi, and . Vignudelli, On the Discriminating Power of Testing Equivalences for Reactive Probabilistic Systems: Results and Open Problems, Proc. QEST'14, pp.281-296, 2014.

U. [. Crubillé and . Dal-lago, On Probabilistic Applicative Bisimulation and Call-by-Value ??-Calculi, Proc. ESOP'14, pp.209-228, 2014.
DOI : 10.1007/978-3-642-54833-8_12

U. [. Crubillé and . Dal-lago, Metric Reasoning about ?-Terms: The Affine Case, Proc. LICS'15, pp.633-644, 2015.

U. [. Crubillé, D. Dal-lago, V. Sangiorgi, and . Vignudelli, On Applicative Similarity, Sequentiality, and Full Abstraction, Correct System Design Platzer, and H. Wehrheim. LNCS 9360, pp.65-82, 2015.
DOI : 10.1016/j.tcs.2004.10.021

G. Castagna, J. Vitek, and F. Z. Nardelli, The Seal Calculus, Information and Computation, vol.201, issue.1, pp.1-54, 2005.
DOI : 10.1016/j.ic.2004.11.005
URL : https://hal.archives-ouvertes.fr/hal-00152521

W. [. Deng and . Du, Probabilistic Barbed Congruence, Electronic Notes in Theoretical Computer Science, vol.190, issue.3, pp.185-203, 2007.
DOI : 10.1016/j.entcs.2007.07.011
URL : https://doi.org/10.1016/j.entcs.2007.07.011

W. [. Deng and . Du, Logical, Metric, and Algorithmic Characterisations of Probabilistic Bisimulation, 2011.

]. Y. Den14 and . Deng, Semantics of Probabilistic Processes. An Operational Approach, 2014.

J. Desharnais, A. Edalat, and P. Panangaden, Bisimulation for Labelled Markov Processes, Information and Computation, vol.179, issue.2, pp.163-193, 2002.
DOI : 10.1006/inco.2001.2962
URL : https://doi.org/10.1006/inco.2001.2962

R. [. Deng, M. Glabbeek, C. Hennessy, and . Morgan, Characterising Testing Preorders for Finite Probabilistic Processes, In: Logical Methods in Computer Science, vol.4, issue.4, pp.4-5, 2008.
DOI : 10.2168/lmcs-4(4:4)2008

R. [. Deng, M. Glabbeek, C. Hennessy, and . Morgan, Testing Finitary Probabilistic Processes, Proc. CONCUR'09, pp.274-288, 2009.
DOI : 10.1007/978-3-642-04081-8_19

]. Y. Dghmz07a, R. Deng, M. Glabbeek, C. Hennessy, C. Morgan et al., Characterising Testing Preorders for Finite Probabilistic Processes, Proc. LICS'07, pp.313-325, 2007.

R. [. Danos and . Harmer, Probabilistic Game Semantics, In: ACM Trans. Comput. Logic, vol.33, pp.359-382, 2002.
DOI : 10.1145/507382.507385

[. Nicola and M. Hennessy, Testing equivalences for processes, Theoretical Computer Science, vol.34, issue.1-2, pp.83-133, 1984.
DOI : 10.1016/0304-3975(84)90113-0

R. [. Desharnais, V. Jagadeesan, P. Gupta, and . Panangaden, The metric analogue of weak bisimulation for probabilistic processes, Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, pp.413-422, 2002.
DOI : 10.1109/LICS.2002.1029849

M. [. Argenio and . Lee, Probabilistic Transition System Specification: Congruence and Full Abstraction of Bisimulation, Proc. FoSSaCS'12, pp.452-466, 2012.
DOI : 10.1007/978-3-642-28729-9_30

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

F. [. Desharnais, M. Laviolette, and . Tracol, Approximate Analysis of Probabilistic Processes: Logic, Simulation and Games, 2008 Fifth International Conference on Quantitative Evaluation of Systems, pp.264-273, 2008.
DOI : 10.1109/QEST.2008.42

A. Liguoro and . Piperno, Nondeterministic Extensions of Untyped ??-Calculus, Information and Computation, vol.122, issue.2, pp.149-177, 1995.
DOI : 10.1006/inco.1995.1145

[. Lago and M. Zorzi, Probabilistic operational semantics for the lambda calculus, RAIRO -Theoretical Informatics and Applications, pp.413-450, 2012.
DOI : 10.1051/ita/2012012
URL : https://hal.archives-ouvertes.fr/hal-00909373

C. [. Ehrhard, M. Tasson, and . Pagani, Probabilistic coherence spaces are fully abstract for probabilistic PCF, Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, pp.309-320
DOI : 10.1145/2535838.2535865

T. [. Godskesen and . Hildebrandt, Extending Howe???s Method to Early Bisimulations for Typed Mobile Embedded Resources with Local Names, Proc. FSTTCS'05, pp.140-151, 2005.
DOI : 10.1007/11590156_11

. [. Goubault-larrecq, Full abstraction for non-deterministic and probabilistic extensions of PCF I: The angelic cases, Journal of Logical and Algebraic Methods in Programming, vol.84, issue.1, pp.155-184, 2015.
DOI : 10.1016/j.jlamp.2014.09.003

]. R. Gla01 and . Glabbeek, The Linear Time -Branching Time Spectrum I. The Semantics of Concrete, Sequential Processes In: Handbook of Process Algebra, pp.3-99, 2001.

]. N. Goo13 and . Goodman, The principles and practice of probabilistic programming, Proc. POPL'13. 2013, pp.399-402

F. [. Groote and . Vaandrager, Structured operational semantics and bisimulation as a congruence, Information and Computation, vol.100, issue.2, pp.202-260, 1992.
DOI : 10.1016/0890-5401(92)90013-6
URL : https://doi.org/10.1016/0890-5401(92)90013-6

D. [. Hur, G. Dreyer, V. Neis, and . Vafeiadis, The marriage of bisimulations and Kripke logical relations, Proc. POPL'12. 2012, pp.59-72

M. Hennessy, Exploring probabilistic bisimulations, part I, Formal Aspects of Computing, vol.6, issue.5, pp.749-768, 2012.
DOI : 10.1007/BF01211867

R. [. Hennessy and . Milner, Algebraic laws for nondeterminism and concurrency, Journal of the ACM, vol.32, issue.1, pp.137-161, 1985.
DOI : 10.1145/2455.2460
URL : https://www.scss.tcd.ie/Matthew.Hennessy/pubs/old/HMjacm85.pdf

]. D. How89 and . Howe, Equality In Lazy Computation Systems, Proc. LICS'89, pp.198-203, 1989.

]. D. How96 and . Howe, Proving Congruence of Bisimulation in Functional Programming Languages, pp.103-112, 1996.

L. [. Huynh and . Tian, On Some Equivalence Relations for Probabilistic Processes, Fundamenta Informaticae, vol.17, pp.211-234, 1992.

C. [. Jonsson, W. Ho-stuart, and . Yi, Testing and refinement for nondeterministic and probabilistic processes, Proc. FTRTFT'94, pp.418-430, 1994.
DOI : 10.1007/3-540-58468-4_176
URL : http://www.docs.uu.se/docs/rtmv/papers/ftrtft94b.ps.gz

B. Jonsson and K. G. Larsen, Specification and refinement of probabilistic processes, [1991] Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science, pp.266-277, 1991.
DOI : 10.1109/LICS.1991.151651

]. C. Jon90 and . Jones, Probabilistic Non-Determinism, 1990.

R. Jagadeesan, C. Pitcher, and J. Riely, Open Bisimulation for Aspects, In: T. Aspect-Oriented Software Development, vol.5, pp.72-132, 2009.
DOI : 10.1145/1218563.1218577
URL : http://fpl.cs.depaul.edu/cpitcher/research/aosd-2007-open-bisimulation-for-aspects-full-version.pdf

B. Jacobs and J. Rutten, An introduction to (co)algebra and (co)induction, Ed. by D. Sangiorgi and J. Rutten, vol.52, issue.2, pp.38-99, 2012.
DOI : 10.1017/CBO9780511792588.003
URL : http://www.cwi.nl/%7Ejanr/papers/files-of-papers/2011_Jacobs_Rutten_new.pdf

J. [. Jeffrey and . Rathke, Towards a theory of bisimulation for local names, Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158), pp.56-66, 1999.
DOI : 10.1109/LICS.1999.782586

[. Jou and S. Smolka, Equivalences, congruences, and complete axiomatizations for probabilistic processes, Proc. CONCUR'90, pp.367-383, 1990.
DOI : 10.1007/BFb0039071

N. [. Jaber and . Tabareau, Kripke Open Bisimulation -A Marriage of Game Semantics and Operational Techniques, Proc. APLAS'15. 2015, pp.271-291

B. Jonsson and W. Yi, Compositional testing preorders for probabilistic processes, Proceedings of Tenth Annual IEEE Symposium on Logic in Computer Science, pp.431-441, 1995.
DOI : 10.1109/LICS.1995.523277

M. [. Koutavas and . Hennessy, Symbolic Bisimulation for a Higher-Order Distributed Language with Passivation, Proc. CONCUR'13, pp.167-181, 2013.
DOI : 10.1007/978-3-642-40184-8_13
URL : https://www.scss.tcd.ie/Matthew.Hennessy/pubs/2013/hopass-concur13.pdf

P. [. Koutavas, E. Levy, and . 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
URL : https://doi.org/10.1016/j.entcs.2011.09.023

G. [. Kwiatkowska and . Norman, A Testing Equivalence for Reactive Probabilistic Processes, Proc. EXPRESS'98, pp.114-132, 1998.
DOI : 10.1016/S1571-0661(04)00121-5
URL : https://doi.org/10.1016/s1571-0661(04)00121-5

]. V. Kw06a, M. Koutavas, and . Wand, Bisimulations for Untyped Imperative Objects, Proc. ESOP'06, pp.146-161, 2006.

]. V. Kw06b, M. Koutavas, and . Wand, Small Bisimulations for Reasoning About Higher-Order Imperative Programs, Proc. POPL'06, pp.141-152, 2006.

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

P. [. Lassen and . Levy, Typed Normal Form Bisimulation, Proc. CSL'07, pp.283-297, 2007.
DOI : 10.1007/978-3-540-74915-8_23
URL : http://www.cs.bham.ac.uk/~pbl/papers/LassenLevy2007tnfb-4.pdf

K. Larsen and A. Skou, Bisimulation through probabilistic testing, Information and Computation, vol.94, issue.1, pp.1-28, 1991.
DOI : 10.1016/0890-5401(91)90030-6
URL : https://doi.org/10.1016/0890-5401(91)90030-6

]. S. Lss09a, A. Lenglet, J. Schmitt, and . Stefani, Howe's Method for Calculi with Passivation, Proc. CONCUR'09, pp.448-462, 2009.

]. S. Lss09b, A. Lenglet, J. Schmitt, and . Stefani, Normal Bisimulations in Calculi with Passivation, Proc. FoSSaCS'09, pp.257-271, 2009.

A. [. Lenglet, J. Schmitt, and . Stefani, Characterizing contextual equivalence in calculi with passivation, Information and Computation, vol.209, issue.11, pp.1390-1433, 2011.
DOI : 10.1016/j.ic.2011.08.002
URL : https://hal.archives-ouvertes.fr/hal-00903877

R. Lanotte and S. Tini, Probabilistic bisimulation as a congruence, ACM Transactions on Computational Logic, vol.10, issue.2, 2009.
DOI : 10.1145/1462179.1462181

]. R. Mil06 and . Milner, Pure bigraphs: Structure and dynamics, In: Inf. Comput, vol.2041, pp.60-122, 2006.

]. R. Mil80 and . Milner, A Calculus of Communicating Systems, Lecture Notes in Computer Science, vol.92, 1980.

]. R. Mil89 and . Milner, Communication and Concurrency, 1989.

]. J. Mit96 and . Mitchell, Foundations for Programming Languages, 1996.

J. Morris, Lambda-calculus models of programming languages, 1968.

J. Maraist, M. Odersky, D. N. Turner, and P. Wadler, Call-by-name, Callby-value , Call-by-need and the Linear lambda Calculus, In: Theoretical Computer Science, vol.228, pp.1-2, 1999.
DOI : 10.1016/s0304-3975(98)00358-2
URL : https://doi.org/10.1016/s0304-3975(98)00358-2

R. Milner and D. Sangiorgi, Barbed bisimulation, Proc. ICALP'92, pp.685-695, 1992.
DOI : 10.1007/3-540-55719-9_114

M. [. Milner, R. Tofte, D. Harper, and . Macqueen, The Definition of Standard ML (Revised), 1997.

G. Neis, Pilsner: A Compositionally Verified Compiler for a Higherorder Imperative Language, Proc. ICFP'15, pp.166-178, 2015.
DOI : 10.1145/2784731.2784764
URL : http://www.mpi-sws.org/%7Edreyer/papers/pilsner/paper.pdf

]. R. Nic87 and . Nicola, Extensional Equivalences for Transition Systems, Acta Informatica, vol.24, pp.211-237, 1987.

]. L. Ong93 and . 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

]. D. Par81 and . Park, Concurrency and Automata on Infinite Sequences, Proc. 5th GI Conference on Theoretical Computer Science, pp.167-183, 1981.

]. A. Pfe01 and . Pfeffer, IBAL: A Probabilistic Rational Programming Language, pp.733-740, 2001.

]. I. Phi87 and . Phillips, Refusal Testing, In: Theoretical Computer Science, vol.50, pp.241-284, 1987.

]. B. Pie02 and . Pierce, Types and Programming Languages, 2002.

]. A. Pit05 and . Pitts, Typed Operational Reasoning Advanced Topics in Types and Programming Languages, pp.245-289, 2005.

]. A. Pit12 and . Pitts, Howe's Method for Higher-order Languages Advanced Topics in Bisimulation and Coinduction Cambridge Tracts in Theoretical Computer Science, Ed. by D. Sangiorgi and J. Rutten, vol.52, issue.5, pp.197-232, 2012.

G. D. Plotkin, LCF considered as a programming language, Theoretical Computer Science, vol.5, issue.3, pp.223-255, 1977.
DOI : 10.1016/0304-3975(77)90044-5
URL : https://doi.org/10.1016/0304-3975(77)90044-5

F. [. Park, S. Pfenning, and . Thrun, A probabilistic language based on sampling functions, ACM Transactions on Programming Languages and Systems, vol.31, issue.1, 2008.
DOI : 10.1145/1452044.1452048
URL : http://www.postech.ac.kr/~gla/paper/a4-park.pdf

E. [. Piérard and . Sumii, Sound Bisimulations for Higher-Order Distributed Process Calculus, Proc. FoSSaCS'11, pp.123-137, 2011.
DOI : 10.1145/1284320.1284325

]. A. Ps12a, E. Piérard, and . Sumii, A Higher-Order Distributed Calculus with Name Creation, Proc. LICS'12. 2012, pp.531-540

D. Pous and D. Sangiorgi, Enhancements of the bisimulation proof method Advanced Topics in Bisimulation and Coinduction, 2012.

J. Rutten and B. Jacobs, Algebras and (Co)Induction " . In: Advanced Topics in Bisimulation and Coinduction, 2012.

A. [. Ramsey and . Pfeffer, Stochastic lambda calculus and monads of probability distributions, Proc. POPL'02, pp.154-165, 2002.
DOI : 10.1145/503272.503288
URL : http://www.eecs.harvard.edu/~nr/pubs/pmonad.ps

]. D. San12a and . Sangiorgi, Introduction to Bisimulation and Coinduction, 2012.

D. Sangiorgi, On the origins of bisimulation and coinduction Advanced Topics in Bisimulation and Coinduction Cambridge Tracts in Theoretical Computer Science, Ed. by D. Sangiorgi and J. Rutten, vol.52, issue.1, pp.1-37, 2012.

]. D. San92 and . Sangiorgi, Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigms, 1992.

]. D. San94 and . Sangiorgi, The Lazy Lambda Calculus in a Concurrency Scenario, In: Information and Computation, vol.111, issue.1, pp.120-153, 1994.

]. D. San97 and . Sands, From SOS Rules to Proof Principles: An Operational Metatheory for Functional Languages, Proc. POPL'97, pp.428-441, 1997.

. [. Saheb-djahromi, Probabilistic LCF, Proc. MFCS'78, pp.442-451, 1978.
DOI : 10.1007/3-540-08921-7_92

]. R. Seg95 and . Segala, Modeling and Verification of Randomized Distributed Real- Time Systems, 1995.

]. R. Seg96 and . Segala, Testing Probabilistic Automata, Proc. CONCUR'96. LNCS 1119, pp.299-314, 1996.

P. Sewell, Acute: High-level Programming Language Design for Distributed Computation, Journal of Functional Programming, vol.17, pp.4-5, 2007.
URL : https://hal.archives-ouvertes.fr/inria-00070671

N. [. Sangiorgi, E. Kobayashi, . Sumii, and . English, Logical Bisimulations and Functional Languages, Proc. FSEN'07, pp.364-379, 2007.
DOI : 10.1007/978-3-540-75698-9_24

N. [. Sangiorgi, E. Kobayashi, and . Sumii, Environmental Bisimulations for Higher-Order Languages, In: ACM Transactions on Programming Languages and Systems, vol.331, p.5, 2011.
DOI : 10.1109/lics.2007.17
URL : https://hal.archives-ouvertes.fr/hal-01337665

S. [. Støvring and . Lassen, A Complete, Co-inductive Syntactic Theory of Sequential Control and State, Proc. POPL'07, pp.161-172, 2007.

R. Segala and N. Lynch, Probabilistic simulations for probabilistic processes, In: Nordic Journal of Computing, vol.2, issue.2, pp.250-273, 1995.
DOI : 10.1007/bfb0015027
URL : http://theory.lcs.mit.edu/tds/papers/Segala/NJC95.ps.gz

]. E. Sp07a, B. C. Sumii, and . Pierce, A Bisimulation for Dynamic Sealing A preliminary version in, Proc. POPL'04, pp.1-3, 2004.

]. E. Sp07b, B. C. Sumii, and . Pierce, A bisimulation for type abstraction and recursion A preliminary version, Proc. POPL'05, 2005.

A. Schmitt and J. Stefani, The M-calculus: a Higher-Order Distributed Process Calculus, Proc. POPL'03, pp.50-61, 2003.
DOI : 10.1145/604131.604136
URL : https://hal.archives-ouvertes.fr/inria-00072227

J. [. Schmitt and . Stefani, The Kell Calculus: A Family of Higher-Order Distributed Process Calculi, Proc. GC'04, pp.146-178, 2005.
DOI : 10.1109/LICS.2000.855782

E. [. Sato and . Sumii, The Higher-Order, Call-by-Value Applied Pi-Calculus, Proc. APLAS'09, pp.311-326, 2009.
DOI : 10.1007/978-3-642-10672-9_22

E. [. Sokolova and . Vink, Probabilistic Automata: System Types, Parallel Composition and Comparison, In: Validation of Stochastic Systems. LNCS, vol.2925, pp.1-43, 2004.
DOI : 10.1007/978-3-540-24611-4_1
URL : http://www.ics.ele.tue.nl/~svlad/ees5202/publications/lncs2925.pdf

V. [. Sangiorgi and . Vignudelli, Environmental Bisimulations for Probabilistic Higher-order Languages, Proc. POPL'16, pp.595-607, 2016.
DOI : 10.1145/2914770.2837651
URL : https://hal.archives-ouvertes.fr/hal-01337665

H. [. Staton, F. Yang, C. Wood, O. Heunen, and . Kammar, Semantics for probabilistic programming, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, pp.525-534
DOI : 10.1007/978-3-642-85473-6

]. B. Tho93 and . Thomsen, Plain CHOCS, A Second Generation Calculus for Higher- Order Processes, Acta Informatica, vol.30, pp.1-59, 1993.

K. [. Yi and . Larsen, Testing Probabilistic and Nondeterministic Processes, Proc. PSTV'92, pp.47-61, 1992.
DOI : 10.1016/B978-0-444-89874-6.50010-6