@inproceedings{07a7c17e381445949a0f07e7f29a9dca,
title = "Relational reasoning via probabilistic coupling",
abstract = "Probabilistic coupling is a powerful tool for analyzing pairs of probabilistic processes. Roughly, coupling two processes requires finding an appropriate witness process that models both processes in the same probability space. Couplings are powerful tools proving properties about the relation between two processes, include reasoning about convergence of distributions and stochastic dominance—a probabilistic version of a monotonicity property. While the mathematical definition of coupling looks rather complex and cumbersome to manipulate, we show that the relational program logic pRHL—the logic underlying the EasyCrypt cryptographic proof assistant—already internalizes a generalization of probabilistic coupling. With this insight, constructing couplings is no harder than constructing logical proofs.We demonstrate how to express and verify classic examples of couplings in pRHL, and we mechanically verify several couplings in EasyCrypt.",
author = "Gilles Barthe and Thomas Espitau and Benjamin Gr{\'e}goire and Justin Hsu and L{\'e}o Stefanesco and Strub, \{Pierre Yves\}",
note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 2015.; 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2015 ; Conference date: 24-11-2015 Through 28-11-2015",
year = "2015",
month = jan,
day = "1",
doi = "10.1007/978-3-662-48899-7\_27",
language = "English",
isbn = "9783662488980",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "387--401",
editor = "Andrei Voronkov and Ansgar Fehnker and Martin Davis and Annabelle McIver",
booktitle = "Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Proceedings",
}