{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,23]],"date-time":"2026-08-23T17:15:45Z","timestamp":1787505345534,"version":"build-2736575974"},"reference-count":51,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2022,8,29]],"date-time":"2022-08-29T00:00:00Z","timestamp":1661731200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100019180","name":"HORIZON EUROPE European Research Council","doi-asserted-by":"publisher","award":["101039196"],"award-info":[{"award-number":["101039196"]}],"id":[{"id":"10.13039\/100019180","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000006","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N00014-19-1-2292"],"award-info":[{"award-number":["N00014-19-1-2292"]}],"id":[{"id":"10.13039\/100000006","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Atracci\u00f3n de Talento","award":["2019-T2\/TIC-13455"],"award-info":[{"award-number":["2019-T2\/TIC-13455"]}]},{"name":"Juan de la Cierva","award":["IJC2019-041599-I"],"award-info":[{"award-number":["IJC2019-041599-I"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,8,29]]},"abstract":"<jats:p>We enhance refinement types with mechanisms to reason about relational properties of probabilistic computations. Our mechanisms, which are inspired from probabilistic couplings, are applicable to a rich set of probabilistic properties, including expected sensitivity, which ensures that the distance between outputs of two probabilistic computations can be controlled from the distance between their inputs. We implement our mechanisms in the type system of Liquid Haskell and we use them to formally verify Haskell implementations of two classic machine learning algorithms: Temporal Difference (TD) reinforcement learning and stochastic gradient descent (SGD). We formalize a fragment of our system for discrete distributions and we prove soundness with respect to a set-theoretical semantics.<\/jats:p>","DOI":"10.1145\/3547643","type":"journal-article","created":{"date-parts":[[2022,8,31]],"date-time":"2022-08-31T15:39:26Z","timestamp":1661960366000},"page":"596-624","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Safe couplings: coupled refinement types"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5983-3347","authenticated-orcid":false,"given":"Elizaveta","family":"Vasilenko","sequence":"first","affiliation":[{"name":"IMDEA Software Institute, Spain \/ HSE University, Russia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0732-5476","authenticated-orcid":false,"given":"Niki","family":"Vazou","sequence":"additional","affiliation":[{"name":"IMDEA Software Institute, Spain"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3853-1777","authenticated-orcid":false,"given":"Gilles","family":"Barthe","sequence":"additional","affiliation":[{"name":"MPI-SP, Germany \/ IMDEA Software Institute, Spain"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,8,31]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Near","author":"Abuah Chike","year":"2021","unstructured":"Chike Abuah , David Darais , and Joseph P . Near . 2021 . Solo : Enforcing Differential Privacy Without Fancy Types. In CoRR. arxiv:2105.01632 Chike Abuah, David Darais, and Joseph P. Near. 2021. Solo: Enforcing Differential Privacy Without Fancy Types. In CoRR. arxiv:2105.01632"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473598"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110265"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434333"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473592"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428240"},{"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\/2535838.2535847"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677000"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480894"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22792-9_5"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1017\/9781108770750.006"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103670"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00145-019-09341-z"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1162\/153244302760200704"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314603"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-45198-4"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429113"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167090"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360592"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371092"},{"key":"e_1_2_1_22_1","volume-title":"Train Faster","author":"Hardt Moritz","unstructured":"Moritz Hardt , Ben Recht , and Yoram Singer . 2016. Train Faster , Generalize Better : Stability of Stochastic Gradient Descent. In ICML. https:\/\/dl.acm.org\/doi\/10.5555\/3045390.3045520 Moritz Hardt, Ben Recht, and Yoram Singer. 2016. Train Faster, Generalize Better: Stability of Stochastic Gradient Descent. In ICML. https:\/\/dl.acm.org\/doi\/10.5555\/3045390.3045520"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-43144-4_30"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-01090-4_23"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1567-8326(02)00065-6"},{"key":"e_1_2_1_26_1","volume-title":"Bunched Fuzz: Sensitivity for Vector Metrics. In CoRR. https:\/\/doi.org\/10.48550\/arXiv.2202.01901","author":"de Amorim Arthur Azevedo","year":"2022","unstructured":"june wunder and Arthur Azevedo de Amorim and Patrick Baillot and Marco Gaboardi . 2022 . Bunched Fuzz: Sensitivity for Vector Metrics. In CoRR. https:\/\/doi.org\/10.48550\/arXiv.2202.01901 june wunder and Arthur Azevedo de Amorim and Patrick Baillot and Marco Gaboardi. 2022. Bunched Fuzz: Sensitivity for Vector Metrics. In CoRR. https:\/\/doi.org\/10.48550\/arXiv.2202.01901"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(85)90012-1"},{"key":"e_1_2_1_28_1","volume-title":"STORM: Refinement Types for Secure Web Applications. In OSDI. https:\/\/www.usenix.org\/conference\/osdi21\/presentation\/lehmann","author":"Lehmann Nico","year":"2021","unstructured":"Nico Lehmann , Rose Kunkel , Jordan Brown , Jean Yang , Niki Vazou , Nadia Polikarpova , Deian Stefan , and Ranjit Jhala . 2021 . STORM: Refinement Types for Secure Web Applications. In OSDI. https:\/\/www.usenix.org\/conference\/osdi21\/presentation\/lehmann Nico Lehmann, Rose Kunkel, Jordan Brown, Jean Yang, Niki Vazou, Nadia Polikarpova, Deian Stefan, and Ranjit Jhala. 2021. STORM: Refinement Types for Secure Web Applications. In OSDI. https:\/\/www.usenix.org\/conference\/osdi21\/presentation\/lehmann"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1137\/1035121"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3452096"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371072"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/229542.229547"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2011.12"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360598"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192394"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46666-7_4"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503288"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863568"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2887747.2804317"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2914770.2837655"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-94821-8_33"},{"key":"e_1_2_1_42_1","doi-asserted-by":"crossref","unstructured":"Hermann Thorisson. 2000. Coupling Stationarity and Regeneration. Springer. https:\/\/notendur.hi.is\/hermann\/iid\/csr\/ \t\t\t\t  Hermann Thorisson. 2000. Coupling Stationarity and Regeneration. Springer. https:\/\/notendur.hi.is\/hermann\/iid\/csr\/","DOI":"10.1007\/978-1-4612-1236-2"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.6710298"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3242744.3242756"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2775050.2633366"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2692915.2628161"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158141"},{"key":"e_1_2_1_48_1","volume-title":"Optimal Transport, old and new","author":"Villani C\u00e9dric","unstructured":"C\u00e9dric Villani . 2009. Optimal Transport, old and new . Springer . https:\/\/link.springer.com\/book\/10.1007\/978-3-540-71050-9 C\u00e9dric Villani. 2009. Optimal Transport, old and new. Springer. https:\/\/link.springer.com\/book\/10.1007\/978-3-540-71050-9"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371093"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110254"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341697"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3547643","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3547643","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3547643","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T14:43:29Z","timestamp":1750257809000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3547643"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,8,29]]},"references-count":51,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2022,8,29]]}},"alternative-id":["10.1145\/3547643"],"URL":"https:\/\/doi.org\/10.1145\/3547643","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,8,29]]},"assertion":[{"value":"2022-08-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}