{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T07:42:57Z","timestamp":1770277377496,"version":"3.49.0"},"reference-count":41,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2017,12,27]],"date-time":"2017-12-27T00:00:00Z","timestamp":1514332800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"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"}]},{"DOI":"10.13039\/100000144","name":"Division of Computer and Network Systems","doi-asserted-by":"publisher","award":["1513694"],"award-info":[{"award-number":["1513694"]}],"id":[{"id":"10.13039\/100000144","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["679127"],"award-info":[{"award-number":["679127"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2018,1]]},"abstract":"<jats:p>Program sensitivity, also known as Lipschitz continuity, describes how small changes in a program\u2019s input lead to bounded changes in the output. We propose an average notion of program sensitivity for probabilistic programs\u2014expected sensitivity\u2014that averages a distance function over a probabilistic coupling of two output distributions from two similar inputs. By varying the distance, expected sensitivity recovers useful notions of probabilistic function sensitivity, including stability of machine learning algorithms and convergence of Markov chains.<\/jats:p>\n          <jats:p>Furthermore, expected sensitivity satisfies clean compositional properties and is amenable to formal verification. We develop a relational program logic called EpRHL for proving expected sensitivity properties. Our logic features two key ideas. First, relational pre-conditions and post-conditions are expressed using distances, a real-valued generalization of typical boolean-valued (relational) assertions. Second, judgments are interpreted in terms of expectation coupling, a novel, quantitative generalization of probabilistic couplings which supports compositional reasoning.<\/jats:p>\n          <jats:p>We demonstrate our logic on examples beyond the reach of prior relational logics. Our main example formalizes uniform stability of the stochastic gradient method. Furthermore, we prove rapid mixing for a probabilistic model of population dynamics. We also extend our logic with a transitivity principle for expectation couplings to capture the path coupling proof technique by Bubley and Dyer, and formalize rapid mixing of the Glauber dynamics from statistical physics.<\/jats:p>","DOI":"10.1145\/3158145","type":"journal-article","created":{"date-parts":[[2017,12,29]],"date-time":"2017-12-29T14:21:49Z","timestamp":1514557309000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":24,"title":["Proving expected sensitivity of probabilistic programs"],"prefix":"10.1145","volume":"2","author":[{"given":"Gilles","family":"Barthe","sequence":"first","affiliation":[{"name":"IMDEA Software Institute, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Espitau","sequence":"additional","affiliation":[{"name":"UPMC, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Benjamin","family":"Gr\u00e9goire","sequence":"additional","affiliation":[{"name":"Inria, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Justin","family":"Hsu","sequence":"additional","affiliation":[{"name":"University College London, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pierre-Yves","family":"Strub","sequence":"additional","affiliation":[{"name":"\u00c9cole Polytechnique, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2017,12,27]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2746325.2746335"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009890"},{"key":"e_1_2_2_3_1","first-page":"912","article-title":"Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model","volume":"2016","author":"Barthe Gilles","year":"2016","unstructured":"Gilles Barthe , Fran\u00e7ois Dupressoir , Sebastian Faust , Benjamin Gr\u00e9goire , Fran\u00e7ois-Xavier Standaert , and Pierre-Yves Strub . 2016 a. Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model . IACR Cryptology ePrint Archive 2016 (2016), 912 . http:\/\/eprint.iacr.org\/2016\/912 Gilles Barthe, Fran\u00e7ois Dupressoir, Sebastian Faust, Benjamin Gr\u00e9goire, Fran\u00e7ois-Xavier Standaert, and Pierre-Yves Strub. 2016a. Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model. IACR Cryptology ePrint Archive 2016 (2016), 912. http:\/\/eprint.iacr.org\/2016\/912","journal-title":"IACR Cryptology ePrint Archive"},{"key":"e_1_2_2_4_1","volume-title":"Foundations of Security Analysis and Design VII (FOSAD) (Lecture Notes in Computer Science)","author":"Barthe Gilles","unstructured":"Gilles Barthe , Fran\u00e7ois Dupressoir , Benjamin Gr\u00e9goire , C\u00e9sar Kunz , Benedikt Schmidt , and Pierre-Yves Strub . 2013. EasyCrypt: A Tutorial . In Foundations of Security Analysis and Design VII (FOSAD) (Lecture Notes in Computer Science) , Vol. 8604 . Springer-Verlag , 146\u2013166. Tutorial Lectures. Gilles Barthe, Fran\u00e7ois Dupressoir, Benjamin Gr\u00e9goire, C\u00e9sar Kunz, Benedikt Schmidt, and Pierre-Yves Strub. 2013. EasyCrypt: A Tutorial. In Foundations of Security Analysis and Design VII (FOSAD) (Lecture Notes in Computer Science), Vol. 8604. Springer-Verlag, 146\u2013166. Tutorial Lectures."},{"key":"e_1_2_2_5_1","volume-title":"International Colloquium on Automata, Languages and Programming (ICALP)","author":"Barthe Gilles","unstructured":"Gilles Barthe , Thomas Espitau , Justin Hsu , Tetsuya Sato , and Pierre-Yves Strub . 2017a. \u22c6-Liftings for differential privacy . In International Colloquium on Automata, Languages and Programming (ICALP) , Warsaw, Poland (Leibniz International Proceedings in Informatics) , Vol. 80 . Schloss Dagstuhl\u2013Leibniz Center for Informatics , 102:1\u2013102:12. https:\/\/arxiv.org\/abs\/ 1705.00133 Gilles Barthe, Thomas Espitau, Justin Hsu, Tetsuya Sato, and Pierre-Yves Strub. 2017a. \u22c6-Liftings for differential privacy. In International Colloquium on Automata, Languages and Programming (ICALP), Warsaw, Poland (Leibniz International Proceedings in Informatics) , Vol. 80. Schloss Dagstuhl\u2013Leibniz Center for Informatics, 102:1\u2013102:12. https:\/\/arxiv.org\/abs\/ 1705.00133"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978391"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677000"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54110-4_20"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934554"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009896"},{"key":"e_1_2_2_11_1","volume-title":"ACM SIGPLAN\u2013SIGACT Symposium on Principles of Programming Languages (POPL)","author":"Barthe Gilles","year":"2013","unstructured":"Gilles Barthe , Benjamin Gr\u00e9goire , and Santiago Zanella-B\u00e9guelin . 2009. Formal Certification of Code-Based Cryptographic Proofs . In ACM SIGPLAN\u2013SIGACT Symposium on Principles of Programming Languages (POPL) , Savannah, Georgia . New York , 90\u2013101. http:\/\/certicrypt.gforge.inria.fr\/ 2013 .Journal.pdf Gilles Barthe, Benjamin Gr\u00e9goire, and Santiago Zanella-B\u00e9guelin. 2009. Formal Certification of Code-Based Cryptographic Proofs. In ACM SIGPLAN\u2013SIGACT Symposium on Principles of Programming Languages (POPL), Savannah, Georgia. New York, 90\u2013101. http:\/\/certicrypt.gforge.inria.fr\/2013.Journal.pdf"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103670"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39212-2_8"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9904-1976-14091-8"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1162\/153244302760200704"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1997.646111"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706308"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1089\/cmb.2012.0064"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2015.2424951"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/1046920.1046923"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429113"},{"key":"e_1_2_2_22_1","volume-title":"International Conference on Machine Learning (ICML)","volume":"48","author":"Hardt Moritz","year":"2016","unstructured":"Moritz Hardt , Ben Recht , and Yoram Singer . 2016 . Train faster, generalize better: Stability of stochastic gradient descent . In International Conference on Machine Learning (ICML) , New York, NY (Journal of Machine Learning Research) , Vol. 48 . JMLR.org, 1225\u20131234. http:\/\/jmlr.org\/proceedings\/papers\/v48\/hardt16.html Moritz Hardt, Ben Recht, and Yoram Singer. 2016. Train faster, generalize better: Stability of stochastic gradient descent. In International Conference on Machine Learning (ICML), New York, NY (Journal of Machine Learning Research), Vol. 48. JMLR.org, 1225\u20131234. http:\/\/jmlr.org\/proceedings\/papers\/v48\/hardt16.html"},{"key":"e_1_2_2_23_1","volume-title":"Clark","author":"Hartl Daniel L.","year":"2006","unstructured":"Daniel L. Hartl and Andrew G . Clark . 2006 . Principles of Population Genetics (fourth ed.). Sinauer Associates . Daniel L. Hartl and Andrew G. Clark. 2006. Principles of Population Genetics (fourth ed.). Sinauer Associates."},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_1"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17339-4"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1002\/rsa.3240070205"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_15"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_5"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1979.38"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(85)90012-1"},{"key":"e_1_2_2_32_1","volume-title":"Lectures on the coupling method","author":"Lindvall Torgny","unstructured":"Torgny Lindvall . 2002. Lectures on the coupling method . Courier Corporation . Torgny Lindvall. 2002. Lectures on the coupling method. Courier Corporation."},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/229542.229547"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1137\/1.9781611974331.ch36"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863568"},{"key":"e_1_2_2_36_1","volume-title":"Approximate Relational Hoare Logic for Continuous Random Samplings. In Conference on the Mathematical Foundations of Programming Semantics (MFPS)","author":"Sato Tetsuya","year":"2016","unstructured":"Tetsuya Sato . 2016 . Approximate Relational Hoare Logic for Continuous Random Samplings. In Conference on the Mathematical Foundations of Programming Semantics (MFPS) , Pittsburgh, Pennsylvania . http:\/\/arxiv.org\/abs\/1603.01445 Tetsuya Sato. 2016. Approximate Relational Hoare Logic for Continuous Random Samplings. In Conference on the Mathematical Foundations of Programming Semantics (MFPS), Pittsburgh, Pennsylvania . http:\/\/arxiv.org\/abs\/1603.01445"},{"key":"e_1_2_2_37_1","volume-title":"Developing Bug-Free Machine Learning Systems With Formal Mathematics. In International Conference on Machine Learning (ICML)","volume":"70","author":"Selsam Daniel","unstructured":"Daniel Selsam , Percy Liang , and David L. Dill . 2017 . Developing Bug-Free Machine Learning Systems With Formal Mathematics. In International Conference on Machine Learning (ICML) , Sydney, Australia (Proceedings of Machine Learning Research) , Doina Precup and Yee Whye Teh (Eds.) , Vol. 70 . 3047\u20133056. http:\/\/proceedings.mlr.press\/v70\/selsam17a.html Daniel Selsam, Percy Liang, and David L. Dill. 2017. Developing Bug-Free Machine Learning Systems With Formal Mathematics. In International Conference on Machine Learning (ICML), Sydney, Australia (Proceedings of Machine Learning Research) , Doina Precup and Yee Whye Teh (Eds.), Vol. 70. 3047\u20133056. http:\/\/proceedings.mlr.press\/v70\/selsam17a.html"},{"key":"e_1_2_2_38_1","volume-title":"Without-Replacement Sampling for Stochastic Gradient Methods: Convergence Results and Application to Distributed Optimization. CoRR abs\/1603.00570","author":"Shamir Ohad","year":"2016","unstructured":"Ohad Shamir . 2016. Without-Replacement Sampling for Stochastic Gradient Methods: Convergence Results and Application to Distributed Optimization. CoRR abs\/1603.00570 ( 2016 ). http:\/\/arxiv.org\/abs\/1603.00570 Ohad Shamir. 2016. Without-Replacement Sampling for Stochastic Gradient Methods: Convergence Results and Application to Distributed Optimization. CoRR abs\/1603.00570 (2016). http:\/\/arxiv.org\/abs\/1603.00570"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-1236-2"},{"key":"e_1_2_2_40_1","volume-title":"Optimal transport: Old and new","author":"Villani C\u00e9dric","unstructured":"C\u00e9dric Villani . 2008. Optimal transport: Old and new . Springer-Verlag . C\u00e9dric Villani. 2008. Optimal transport: Old and new. Springer-Verlag."},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1137\/1.9781611973730.105"},{"key":"e_1_2_2_42_1","first-page":"1","article-title":"A framework for adaptive differential privacy. In ACM SIGPLAN International Conference on Functional Programming (ICFP), Oxford","volume":"10","author":"Winograd-Cort Daniel","year":"2017","unstructured":"Daniel Winograd-Cort , Andreas Haeberlen , Aaron Roth , and Benjamin C. Pierce . 2017 . A framework for adaptive differential privacy. In ACM SIGPLAN International Conference on Functional Programming (ICFP), Oxford , England. 10 : 1 \u2013 10 :29. https:\/\/dl.acm.org\/citation.cfm?id=3110254 Daniel Winograd-Cort, Andreas Haeberlen, Aaron Roth, and Benjamin C. Pierce. 2017. A framework for adaptive differential privacy. In ACM SIGPLAN International Conference on Functional Programming (ICFP), Oxford, England. 10:1\u201310:29. https:\/\/dl.acm.org\/citation.cfm?id=3110254","journal-title":"England."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158145","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3158145","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3158145","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:11:30Z","timestamp":1750212690000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158145"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,27]]},"references-count":41,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2018,1]]}},"alternative-id":["10.1145\/3158145"],"URL":"https:\/\/doi.org\/10.1145\/3158145","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,12,27]]},"assertion":[{"value":"2017-12-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}