G. Barthe, P. R. Argenio, and T. Rezk, Secure information flow by self-composition, Grégoire, S. Heraud, and S. Zanella-Béguelin, pp.1207-1252, 2011.
DOI : 10.1145/5397.5399

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

G. Barthe, F. Dupressoir, B. Grégoire, C. Kunz, B. Schmidt et al., EasyCrypt: A Tutorial, Foundations of Security Analysis and Design VII, pp.146-166, 2014.
DOI : 10.1007/978-3-642-22792-9_5

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

G. Barthe, T. Espitau, B. Grégoire, J. Hsu, L. Stefanesco et al., Relational Reasoning via Probabilistic Coupling, International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), pp.387-401, 2015.
DOI : 10.1007/978-3-662-48899-7_27

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

G. Barthe, M. Gaboardi, B. Grégoire, J. Hsu, and P. Strub, Proving differential privacy via probabilistic couplings Proving differential privacy via probabilistic couplings Coupling proofs are probabilistic product programs Coupling proofs are probabilistic product programs, IEEE Symposium on Logic in Computer Science (LICS) ACM SIGPLAN?SIGACT Symposium on Principles of Programming Languages (POPL), pp.749-758, 2016.
DOI : 10.1145/2933575.2934554

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

A. Z. Broder, Generating random spanning trees Generating random spanning trees, ACM SIGACT Symposium on Theory of Computing (STOC), pp.442-447, 1989.
DOI : 10.1109/sfcs.1989.63516

R. Chadha, L. Cruz-filipe, P. Mateus, A. Sernadas, and R. Hasheminezhad, Reasoning about probabilistic sequential programs, Theoretical Computer Science, vol.379, issue.1-2, pp.142-165, 2007.
DOI : 10.1016/j.tcs.2007.02.040

URL : http://doi.org/10.1016/j.tcs.2007.02.040

K. Chatterjee, P. Novotný, and D. Zikelic, Stochastic invariants for probabilistic termination Stochastic invariants for probabilistic termination
DOI : 10.1145/3009837.3009873

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

Á. Darvas, R. Hähnle, and D. Sands, A Theorem Proving Approach to Analysis of Secure Information Flow, Security in Pervasive Computing (SPC), pp.193-209, 2005.
DOI : 10.1007/978-3-540-32004-3_20

J. Hartog, Probabilistic extensions of semantical models, 2002.

L. M. Ferrer-fioriti and H. Hermanns, Probabilistic termination: Soundness, completeness , and compositionality, ACM SIGPLAN?SIGACT Symposium on Principles of Programming Languages (POPL), pp.489-501, 2015.

D. Kozen, A probabilistic PDL, Journal of Computer and System Sciences, vol.30, issue.2, pp.162-178, 1985.
DOI : 10.1016/0022-0000(85)90012-1

C. Morgan, A. Mciver, and K. Seidel, Probabilistic predicate transformers, ACM Transactions on Programming Languages and Systems, vol.18, issue.3, pp.325-353, 1996.
DOI : 10.1145/229542.229547

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

J. Pearl and A. Paz, Graphoids: Graph-based logic for reasoning about relevance relations Graphoids: Graph-based logic for reasoning about relevance relations, 1985.

L. H. Ramshaw, Formalizing the Analysis of Algorithms, 1979.

R. Rand and S. Zdancewic, VPHL: A Verified Partial-Correctness Logic for Probabilistic Programs, Conference on the Mathematical Foundations of Programming Semantics (MFPS), 2015.
DOI : 10.1016/j.entcs.2015.12.021

URL : http://doi.org/10.1016/j.entcs.2015.12.021

H. Thorisson, Coupling, Stationarity, and Regeneration, 2000.
DOI : 10.1007/978-1-4612-1236-2

C. Villani, Optimal transport: old and new, 2008.
DOI : 10.1007/978-3-540-71050-9