. [. Qi and . }i?i, {[Qi, if hi then f else g] p i }i?I [Q, let v, w be x, hi] p i }i?I [Q, let e be x, y in g] ? {[Qi, let hi be x, y in g] p i }i?I [Q, meas(r)] ? {[MS r ff (Q), ff] PR r ff (Q) , [MS r tt (Q), tt] PR r tt

M. Gavin and . Bierman, Program equivalence in a linear functional language, J. Funct. Program, vol.10, issue.2, pp.167-190, 2000.

R. L. Crole, Completeness of bisimilarity for contextual equivalence in linear theories, Logic Journal of IGPL, vol.9, issue.1, 2001.
DOI : 10.1093/jigpal/9.1.27

R. Crubillé and U. D. Lago, On Probabilistic Applicative Bisimulation and Call-by-Value ??-Calculi, ESOP, pp.209-228, 2014.
DOI : 10.1007/978-3-642-54833-8_12

U. Dal, L. , and A. Rioli, Applicative bisimulation and quantum ?-calculi (long version) Available at http, 2014.

A. S. Timothy, S. J. Davidson, H. Gay, R. Mlnarik, N. Nagarajan et al., Model checking for communicating quantum processes, IJUC, vol.8, issue.1, pp.73-98, 2012.

Y. Deng and Y. Feng, Open bisimulation for quantum processes. CoRR, abs, 1201.
DOI : 10.1007/978-3-642-33475-7_9

URL : http://arxiv.org/abs/1201.0416

J. Simon, R. Gay, and . Nagarajan, Communicating quantum processes, POPL, pp.145-157, 2005.

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

B. Jacobs, Coalgebraic Walks, in Quantum and Turing Computation, FOS- SACS, pp.12-26, 2011.
DOI : 10.1007/978-3-642-19805-2_2

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.174.6865

V. Koutavas, P. B. Levy, and E. 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 : http://doi.org/10.1016/j.entcs.2011.09.023

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 : http://doi.org/10.1016/0890-5401(91)90030-6

B. Søren, C. Lassen, and . Pitcher, Similarity and bisimilarity for countable non-determinism and higher-order functions, Electr. Notes Theor. Comput. Sci, vol.10, pp.246-266, 1997.

R. Milner, Fully abstract models of typed ??-calculi, Theoretical Computer Science, vol.4, issue.1, pp.1-22, 1977.
DOI : 10.1016/0304-3975(77)90053-6

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

A. M. Pitts, Operationally-Based Theories of Program Equivalence, Semantics and Logics of Computation, pp.241-298, 1997.
DOI : 10.1017/CBO9780511526619.007

G. Plotkin, Lambda definability and logical relations, Memo SAI-RM-4, 1973.

D. Sangiorgi, Introduction to Bisimulation and Coinduction, 2012.
DOI : 10.1017/CBO9780511777110

URL : https://hal.archives-ouvertes.fr/hal-00907026

P. Selinger and B. Valiron, A lambda calculus for quantum computation with classical control, TLCA, pp.354-368, 2005.
DOI : 10.1017/S0960129506005238

URL : https://hal.archives-ouvertes.fr/hal-00483924

P. Selinger and B. Valiron, On a Fully Abstract Model for a Quantum Linear Functional Language, Electronic Notes in Theoretical Computer Science, vol.210, pp.123-137, 2008.
DOI : 10.1016/j.entcs.2008.04.022

M. W. Franck-van-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