{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T08:08:48Z","timestamp":1770278928929,"version":"3.49.0"},"reference-count":33,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T00:00:00Z","timestamp":1609718400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100007015","name":"University of Wisconsin","doi-asserted-by":"crossref","id":[{"id":"10.13039\/100007015","id-type":"DOI","asserted-by":"crossref"}]},{"name":"National Science Foundation SaTC","award":["2023222"],"award-info":[{"award-number":["2023222"]}]},{"name":"National Science Foundation CCF","award":["1943130"],"award-info":[{"award-number":["1943130"]}]},{"DOI":"10.13039\/100005801","name":"Facebook","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100005801","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":[[2021,1,4]]},"abstract":"<jats:p>Sensitivity properties describe how changes to the input of a program affect the output, typically by upper bounding the distance between the outputs of two runs by a monotone function of the distance between the corresponding inputs. When programs are probabilistic, the distance between outputs is a distance between distributions. The Kantorovich lifting provides a general way of defining a distance between distributions by lifting the distance of the underlying sample space; by choosing an appropriate distance on the base space, one can recover other usual probabilistic distances, such as the Total Variation distance. We develop a relational pre-expectation calculus to upper bound the Kantorovich distance between two executions of a probabilistic program. We illustrate our methods by proving algorithmic stability of a machine learning algorithm, convergence of a reinforcement learning algorithm, and fast mixing for card shuffling algorithms. We also consider some extensions: using our calculus to show convergence of Markov chains to the uniform distribution over states and an asynchronous extension to reason about pairs of program executions with different control flow.<\/jats:p>","DOI":"10.1145\/3434333","type":"journal-article","created":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T17:34:24Z","timestamp":1609781664000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":20,"title":["A pre-expectation calculus for probabilistic sensitivity"],"prefix":"10.1145","volume":"5","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6746-2734","authenticated-orcid":false,"given":"Alejandro","family":"Aguirre","sequence":"first","affiliation":[{"name":"IMDEA Software Institute, Spain \/ Universidad Polit\u00e9cnica de Madrid, Spain"}]},{"given":"Gilles","family":"Barthe","sequence":"additional","affiliation":[{"name":"MPI-SP, Germany \/ IMDEA Software Institute, Spain"}]},{"given":"Justin","family":"Hsu","sequence":"additional","affiliation":[{"name":"University of Wisconsin-Madison, USA"}]},{"given":"Benjamin Lucien","family":"Kaminski","sequence":"additional","affiliation":[{"name":"University College London, UK"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6143-1926","authenticated-orcid":false,"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[{"name":"RWTH Aachen University, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9151-0441","authenticated-orcid":false,"given":"Christoph","family":"Matheja","sequence":"additional","affiliation":[{"name":"RWTH Aachen University, Germany \/ ETH Zurich, Switzerland"}]}],"member":"320","published-online":{"date-parts":[[2021,1,4]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"S\u00e9minaire de Probabilit\u00e9s XVII 1981\/82 (Lecture Notes in Mathematics","author":"Aldous David","unstructured":"David Aldous . 1983. Random Walks on Finite Groups and Rapidly Mixing Markov Chains . In S\u00e9minaire de Probabilit\u00e9s XVII 1981\/82 (Lecture Notes in Mathematics , Vol. 986 ). Springer-Verlag , 243-297. https:\/\/eudml.org\/doc\/113445 David Aldous. 1983. Random Walks on Finite Groups and Rapidly Mixing Markov Chains. In S\u00e9minaire de Probabilit\u00e9s XVII 1981\/82 (Lecture Notes in Mathematics, Vol. 986 ). Springer-Verlag, 243-297. https:\/\/eudml.org\/doc\/113445"},{"key":"e_1_2_1_2_1","volume-title":"The 23rd International Conference on Artificial Intelligence and Statistics, AISTATS 2020","volume":"108","author":"Amortila Philip","year":"2020","unstructured":"Philip Amortila , Doina Precup , Prakash Panangaden , and Marc G. Bellemare . 2020. A Distributional Analysis of SamplingBased Reinforcement Learning Algorithms . In The 23rd International Conference on Artificial Intelligence and Statistics, AISTATS 2020 , 26-28 August 2020 , Online [Palermo, Sicily, Italy] (Proceedings of Machine Learning Research , Vol. 108 ), Silvia Chiappa and Roberto Calandra (Eds.). PMLR, 4357-4366. http:\/\/proceedings.mlr.press\/v108\/amortila20a.html Philip Amortila, Doina Precup, Prakash Panangaden, and Marc G. Bellemare. 2020. A Distributional Analysis of SamplingBased Reinforcement Learning Algorithms. In The 23rd International Conference on Artificial Intelligence and Statistics, AISTATS 2020, 26-28 August 2020, Online [Palermo, Sicily, Italy] (Proceedings of Machine Learning Research, Vol. 108 ), Silvia Chiappa and Roberto Calandra (Eds.). PMLR, 4357-4366. http:\/\/proceedings.mlr.press\/v108\/amortila20a.html"},{"key":"e_1_2_1_3_1","volume-title":"Doleans-Dade","author":"Ash Robert B.","year":"2000","unstructured":"Robert B. Ash and Catherine A . Doleans-Dade . 2000 . Probability and Measure Theory. Academic Press . Robert B. Ash and Catherine A. Doleans-Dade. 2000. Probability and Measure Theory. Academic Press."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2746325.2746335"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009890"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209177"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158145"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290347"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434320"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964003"},{"key":"e_1_2_1_11_1","unstructured":"Olivier Bousquet and Andr\u00e9 Elisseef. 2002. Stability and Generalization. Journal of Machine Learning Research 2 ( 2002 ) 499-526. http:\/\/www.jmlr.org\/papers\/v2\/bousquet02a.html  Olivier Bousquet and Andr\u00e9 Elisseef. 2002. Stability and Generalization. Journal of Machine Learning Research 2 ( 2002 ) 499-526. http:\/\/www.jmlr.org\/papers\/v2\/bousquet02a.html"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706308"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2240236.2240262"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429113"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-12(4:12)2016"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2017.09.011"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.peva.2013.11.004"},{"key":"e_1_2_1_18_1","first-page":"1225","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 - 1234 . 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-1234. http:\/\/jmlr.org\/proceedings\/papers\/v48\/hardt16.html"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-01090-4_23"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005153"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_15"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(85)90012-1"},{"key":"e_1_2_1_23_1","volume-title":"Refinement and Proof for Probabilistic Systems","author":"McIver Annabelle","unstructured":"Annabelle McIver and Carroll Morgan . 2005. Abstraction , Refinement and Proof for Probabilistic Systems . Springer . Annabelle McIver and Carroll Morgan. 2005. Abstraction, Refinement and Proof for Probabilistic Systems. Springer."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/229542.229547"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3156018"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2935317"},{"key":"e_1_2_1_27_1","unstructured":"David Park. 1969. Fixpoint Induction and Proofs of Program Properties. Machine Intelligence 5 ( 1969 ).  David Park. 1969. Fixpoint Induction and Proofs of Program Properties. Machine Intelligence 5 ( 1969 )."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00205-016-1026-7"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863568"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00115009"},{"key":"e_1_2_1_31_1","volume-title":"Optimal Transport: Old and New","author":"Villani C\u00e9dric","year":"2008","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_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371093"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110254"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434333","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3434333","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:31:47Z","timestamp":1750195907000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434333"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,4]]},"references-count":33,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2021,1,4]]}},"alternative-id":["10.1145\/3434333"],"URL":"https:\/\/doi.org\/10.1145\/3434333","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,1,4]]},"assertion":[{"value":"2021-01-04","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}