G. Barthe, P. D. Argenio, and T. Rezk, Secure Information Flow by Self- Composition, Computer Security Foundations, CSF'04, pp.100-114, 2004.
DOI : 10.1109/csfw.2004.1310735
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.378.849

G. Barthe, B. Grégoire, and S. Zanella-béguelin, Formal certification of code-based cryptographic proofs, Principles of Programming Languages, POPL'09, pp.90-101, 2009.

G. Barthe, J. M. Crespo, and C. Kunz, Relational Verification Using Product Programs, Formal Methods, 2011.
DOI : 10.1007/978-3-540-68237-0_5
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.476.8936

G. Barthe, B. Grégoire, S. Heraud, and S. Z. Béguelin, Computer-Aided Security Proofs for the Working Cryptographer, Advances in Cryptology ? CRYPTO 2011, pp.71-90, 2011.
DOI : 10.1007/978-3-642-22792-9_5
URL : https://hal.archives-ouvertes.fr/hal-01112075

N. Benton, Simple relational correctness proofs for static analyses and program transformations, Principles of Programming Languages, POPL'04, pp.14-25, 2004.
DOI : 10.1145/982962.964003
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.2.4900

Y. Deng and W. Du, Logical, metric, and algorithmic characterisations of probabilistic bisimulation, 2011.

C. Mufa, Optimal markovian couplings and applications, Acta Mathematica Sinica, vol.14, issue.3, pp.260-275, 1994.
DOI : 10.1080/17442508608833419

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

H. Yang, Relational separation logic, Theoretical Computer Science, vol.375, issue.1-3, pp.308-334, 2007.
DOI : 10.1016/j.tcs.2006.12.036
URL : http://doi.org/10.1016/j.tcs.2006.12.036

A. Zaks and A. Pnueli, CoVaC: Compiler Validation by Program Analysis of the Cross-Product, Formal Methods, pp.35-51, 2008.
DOI : 10.1007/978-3-540-68237-0_5