{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:48:22Z","timestamp":1772164102499,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":57,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"vor","delay-in-days":365,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["TC-1065060 & TWC-1513694"],"award-info":[{"award-number":["TC-1065060 & TWC-1513694"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000893","name":"Simons Foundation","doi-asserted-by":"publisher","award":["#360368"],"award-info":[{"award-number":["#360368"]}],"id":[{"id":"10.13039\/100000893","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,1]]},"DOI":"10.1145\/3009837.3009896","type":"proceedings-article","created":{"date-parts":[[2016,12,22]],"date-time":"2016-12-22T16:20:29Z","timestamp":1482423629000},"page":"161-174","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":25,"title":["Coupling proofs are probabilistic product programs"],"prefix":"10.1145","author":[{"given":"Gilles","family":"Barthe","sequence":"first","affiliation":[{"name":"IMDEA Software Institute, Spain"}]},{"given":"Benjamin","family":"Gr\u00e9goire","sequence":"additional","affiliation":[{"name":"Inria, France"}]},{"given":"Justin","family":"Hsu","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, USA"}]},{"given":"Pierre-Yves","family":"Strub","sequence":"additional","affiliation":[{"name":"IMDEA Software Institute, Spain \/ \u00c9cole Polytechnique, France"}]}],"member":"320","published-online":{"date-parts":[[2017,1]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Shift-coupling. Stochastic Processes and their Applications, 44:1\u201314","author":"Aldous D. J.","year":"1993","unstructured":"D. J. Aldous and H. Thorisson. Shift-coupling. Stochastic Processes and their Applications, 44:1\u201314, 1993."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111046"},{"key":"e_1_3_2_1_3_1","volume-title":"Random walks (lecture notes). Technical report","author":"Avena L.","unstructured":"L. Avena, M. Heydenreich, F. den Hollander, E. Verbitskiy, and W. van Zuijlen. Random walks (lecture notes). Technical report, Mathematical Institute, Leiden University."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/1009380.1009669"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480894"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/2021296.2021319"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103670"},{"key":"e_1_3_2_1_8_1","series-title":"Lecture Notes in Computer Science","first-page":"43","volume-title":"Symposium on the Logical Foundations of Computer Science (LFCS)","author":"Barthe G.","unstructured":"G. Barthe, J. M. Crespo, and C. Kunz. Beyond 2-safety: Asymmetric product programs for relational program verification. In Symposium on the Logical Foundations of Computer Science (LFCS), San Diego, California, volume 7734 of Lecture Notes in Computer Science, pages 29\u201343. Springer-Verlag, 2013."},{"key":"e_1_3_2_1_9_1","series-title":"Lecture Notes in Computer Science","first-page":"166","volume-title":"Foundations of Security Analysis and Design VII (FOSAD)","author":"Barthe G.","unstructured":"G. Barthe, F. Dupressoir, B. Gr\u00e9goire, C. Kunz, B. Schmidt, and P. Strub. Easycrypt: A tutorial. In Foundations of Security Analysis and Design VII (FOSAD), volume 8604 of Lecture Notes in Computer Science, pages 146\u2013166. Springer-Verlag, 2013. Tutorial Lectures."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535847"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2014.36"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48899-7_27"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677000"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2016.05.004"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934554"},{"key":"e_1_3_2_1_16_1","series-title":"Leibniz International Proceedings in Informatics","first-page":"15","volume-title":"International Colloquium on Automata, Languages and Programming (ICALP)","author":"Barthe G.","unstructured":"G. Barthe, M. Gaboardi, B. Gr\u00e9goire, J. Hsu, and P.-Y. Strub. A program logic for union bounds. In International Colloquium on Automata, Languages and Programming (ICALP), Rome, Italy, volume 55 of Leibniz International Proceedings in Informatics, pages 107:1\u2013107:15. Schloss Dagstuhl\u2013Leibniz Center for Informatics, 2016."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964003"},{"key":"e_1_3_2_1_18_1","series-title":"Lecture Notes in Computer Science","first-page":"60","volume-title":"International Conference on Typed Lambda Calculi and Applications (TLCA)","author":"Benton N.","unstructured":"N. Benton, M. Hofmann, and V. Nigam. Proof-relevant logical relations for name generation. In International Conference on Typed Lambda Calculi and Applications (TLCA), Eindhoven, The Netherlands, volume 7941 of Lecture Notes in Computer Science, pages 48\u201360. Springer-Verlag, 2013."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/2033939.2033947"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2007.30"},{"key":"e_1_3_2_1_21_1","volume-title":"International Conference on Foundations of Software Science and Computation Structures (FoSSaCS)","volume":"9034","author":"Bizjak A.","unstructured":"A. Bizjak and L. Birkedal. Step-indexed logical relations for probability. In International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), London, England, volume 9034 of Lecture Notes in Computer Science, pages 279\u2013294. Springer-Verlag, 2015."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1201\/b10905"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/795663.796353"},{"key":"e_1_3_2_1_24_1","volume-title":"A unified indifferentiability proof for permutationor block cipher-based hash functions. IACR Cryptology ePrint Archive","author":"Canteaut A.","year":"2012","unstructured":"A. Canteaut, T. Fuhr, M. Naya-Plasencia, P. Paillier, J. Reinhard, and M. Videau. A unified indifferentiability proof for permutationor block cipher-based hash functions. IACR Cryptology ePrint Archive, 2012: 363, 2012."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254086"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706308"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32004-3_20"},{"key":"e_1_3_2_1_28_1","unstructured":"J. den Hartog. Probabilistic extensions of semantical models. PhD thesis Vrije Universiteit Amsterdam 2002."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1214\/aoap\/1177005980"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1089\/cmb.2012.0064"},{"key":"e_1_3_2_1_31_1","series-title":"Lecture Notes in Computer Science","first-page":"19","volume-title":"International Conference on Foundations of Software Science and Computation Structures (FoSSaCS)","author":"Ghani N.","unstructured":"N. Ghani, F. N. Forsberg, and A. Simpson. Comprehensive parametric polymorphism: Categorical models and type theory. In International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), Eindhoven, The Netherlands, volume 9634 of Lecture Notes in Computer Science, pages 3\u201319. Springer-Verlag, 2016."},{"key":"e_1_3_2_1_32_1","volume-title":"European Symposium on Programming on Research in Computer Security (ESORICS)","volume":"2808","author":"Gomulkiewicz M.","unstructured":"M. Gomulkiewicz, M. Klonowski, and M. Kutylowski. Rapid mixing and security of Chaum\u2019s visual electronic voting. In European Symposium on Programming on Research in Computer Security (ESORICS), Gj\u00f8vic, Norway, volume 2808 of Lecture Notes in Computer Science, pages 132\u2013145. Springer-Verlag."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1002\/rsa.3240070205"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1137\/0218077"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2508859.2516721"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1979.38"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(85)90012-1"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2933610"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1002\/1098-2418(200101)18:1%3C1::AID-RSA1%3E3.0.CO;2-7"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535872"},{"key":"e_1_3_2_1_41_1","volume-title":"Markov chains and mixing times","author":"Levin D. A.","year":"2009","unstructured":"D. A. Levin, Y. Peres, and E. L. Wilmer. Markov chains and mixing times. American Mathematical Society, 2009."},{"key":"e_1_3_2_1_42_1","volume-title":"Courier Corporation","author":"Lindvall T.","year":"2002","unstructured":"T. Lindvall. Lectures on the coupling method. Courier Corporation, 2002."},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1063\/1.1699114"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.5555\/2041552.2041576"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/229542.229547"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2015.33"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2011.12"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.5555\/909003"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837651"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2016.09.043"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2025113.2025133"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908092"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/11547662_24"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"crossref","unstructured":"H. Thorisson. Coupling Stationarity and Regeneration. Springer-Verlag 2000.","DOI":"10.1007\/978-1-4612-1236-2"},{"key":"e_1_3_2_1_55_1","volume-title":"Optimal transport: old and new","author":"Villani C.","year":"2008","unstructured":"C. Villani. Optimal transport: old and new. Springer-Verlag, 2008."},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.036"},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68237-0_5"}],"event":{"name":"POPL '17: The 44th Annual ACM SIGPLAN Symposium on Principles of Programming Languages","location":"Paris France","acronym":"POPL '17","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3009837.3009896","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3009837.3009896","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3009837.3009896","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T09:42:45Z","timestamp":1763458965000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3009837.3009896"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,1]]},"references-count":57,"alternative-id":["10.1145\/3009837.3009896","10.1145\/3009837"],"URL":"https:\/\/doi.org\/10.1145\/3009837.3009896","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/3093333.3009896","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2017,1]]},"assertion":[{"value":"2017-01-01","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}