{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,16]],"date-time":"2025-06-16T16:05:45Z","timestamp":1750089945141,"version":"3.40.5"},"reference-count":62,"publisher":"Cambridge University Press (CUP)","issue":"4-5","license":[{"start":{"date-parts":[[2023,7,31]],"date-time":"2023-07-31T00:00:00Z","timestamp":1690761600000},"content-version":"unspecified","delay-in-days":121,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2023,4]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Several relational program logics have been introduced for integrating reasoning about relational properties of programs and measurement of quantitative difference between computational effects. Toward a general framework for such logics, in this paper, we formalize the concept of quantitative difference between computational effects as <jats:italic>divergences on monads<\/jats:italic>, then develop a relational program logic called <jats:italic>approximate computational relational logic<\/jats:italic> (acRL for short). It supports generic computational effects and divergences on them. The semantics of the acRL is given by <jats:italic>graded strong relational liftings<\/jats:italic> constructed from divergences on monads. We derive two instantiations of the acRL: (1) for the verification of various kinds of differential privacy of higher-order functional probabilistic programs and (2) the other for measuring difference of distributions of cost between higher-order functional probabilistic programs with a cost counting operator.<\/jats:p>","DOI":"10.1017\/s0960129523000245","type":"journal-article","created":{"date-parts":[[2023,7,31]],"date-time":"2023-07-31T05:53:35Z","timestamp":1690782815000},"page":"427-485","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":1,"title":["Divergences on monads for relational program logics"],"prefix":"10.1017","volume":"33","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9895-9209","authenticated-orcid":false,"given":"Tetsuya","family":"Sato","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7529-5489","authenticated-orcid":false,"given":"Shin-ya","family":"Katsumata","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2023,7,31]]},"reference":[{"key":"S0960129523000245_ref54","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(96)80711-0"},{"key":"S0960129523000245_ref48","doi-asserted-by":"publisher","DOI":"10.1143\/JPSJ.18.328"},{"key":"S0960129523000245_ref47","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"S0960129523000245_ref57","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785668"},{"volume-title":"Categorical Logic and Type Theory","year":"1999","author":"Jacobs","key":"S0960129523000245_ref34"},{"key":"S0960129523000245_ref18","doi-asserted-by":"publisher","DOI":"10.1145\/982962.964003"},{"key":"S0960129523000245_ref37","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37075-5_10"},{"key":"S0960129523000245_ref49","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84628-692-6"},{"key":"S0960129523000245_ref2","first-page":"1","article-title":"Synthesizing coupling proofs of differential privacy","volume":"2","author":"Albarghouthi","year":"2018","journal-title":"PACMPL"},{"key":"S0960129523000245_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21437-0_17"},{"key":"S0960129523000245_ref36","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535846"},{"key":"S0960129523000245_ref16","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103670"},{"key":"S0960129523000245_ref4","doi-asserted-by":"publisher","DOI":"10.1215\/ijm\/1255631584"},{"key":"S0960129523000245_ref40","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.2006.881731"},{"key":"S0960129523000245_ref28","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_9"},{"key":"S0960129523000245_ref29","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209149"},{"key":"S0960129523000245_ref30","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0092872"},{"key":"S0960129523000245_ref41","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73564"},{"key":"S0960129523000245_ref23","first-page":"85","article-title":"Eine informationstheoretische Ungleichung und ihre Anwendung auf den beweis der ergodizitat von markoffschen ketten","volume":"8","author":"Csisz\u00e1r","year":"1963","journal-title":"Magyar. Tud. Akad. Mat. Kutato Int. Kozl."},{"key":"S0960129523000245_ref31","unstructured":"Hall, R. (2012). New Statistical Applications for Differential Privacy. PhD thesis, Machine Learning Department School of Computer Science Carnegie Mellon University."},{"key":"S0960129523000245_ref44","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005102"},{"key":"S0960129523000245_ref8","article-title":"Coalgebraic behavioral metrics","volume":"14","author":"Baldan","year":"2018","journal-title":"Logical Methods in Computer Science"},{"key":"S0960129523000245_ref60","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(72)90019-9"},{"key":"S0960129523000245_ref38","article-title":"Codensity lifting of monads and its dual","volume":"14","author":"Katsumata","year":"2018","journal-title":"Logical Methods in Computer Science"},{"key":"S0960129523000245_ref56","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2016.09.043"},{"key":"S0960129523000245_ref9","unstructured":"Balle, B. , Barthe, G. , Gaboardi, M. , Hsu, J. , and Sato, T. (2020). Hypothesis testing interpretations and renyi differential privacy. In Chiappa, S. and Calandra, R. (eds.), Proceedings of the Twenty Third International Conference on Artificial Intelligence and Statistics (AISTATS 2020), vol. 108. Proceedings of Machine Learning Research, Online. PMLR, 2496\u20132506."},{"key":"S0960129523000245_ref24","first-page":"299","article-title":"Information-type measures of difference of probability distributions and indirect observations","volume":"2","author":"Csisz\u00e1r","year":"1967","journal-title":"Studia Scientiarum Mathematicarum Hungarica"},{"key":"S0960129523000245_ref1","doi-asserted-by":"crossref","unstructured":"Albarghouthi, A. and Hsu, J. (2018a). Constraint-based synthesis of coupling proofs. In Computer Aided Verification \u2013 30th International Conference, CAV 2018, Proceedings, Part I, vol. 10981. LNCS. Springer, 327\u2013346.","DOI":"10.1007\/978-3-319-96145-3_18"},{"key":"S0960129523000245_ref12","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2014.36"},{"key":"S0960129523000245_ref15","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009896"},{"key":"S0960129523000245_ref17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39212-2_8"},{"key":"S0960129523000245_ref27","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429113"},{"key":"S0960129523000245_ref50","unstructured":"Olmedo, F. (2014). Approximate Relational Reasoning for Probabilistic Programs. PhD thesis, Technical University of Madrid."},{"key":"S0960129523000245_ref35","unstructured":"Kairouz, P. , Oh, S. , and Viswanath, P. (2015). The composition theorem for differential privacy. In Proceedings of the 32nd International Conference on Machine Learning, ICML 2015, Lille, France, 6-11 July 2015, 1376\u20131385."},{"key":"S0960129523000245_ref45","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2017.11"},{"key":"S0960129523000245_ref53","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863568"},{"key":"S0960129523000245_ref7","article-title":"Extending set functors to generalised metric spaces","volume":"15","author":"Balan","year":"2019","journal-title":"Logical Methods in Computer Science"},{"key":"S0960129523000245_ref42","unstructured":"Mac Lane, S. (1998). Categories for the Working Mathematician (Second Edition), vol. 5. Graduate Texts in Mathematics. Springer."},{"key":"S0960129523000245_ref52","doi-asserted-by":"publisher","DOI":"10.1145\/3158124"},{"key":"S0960129523000245_ref19","unstructured":"Bonchi, F. , K\u00f6nig, B. , and Petrisan, D. (2018). Up-To Techniques for Behavioural Metrics via Fibrations. In 29th International Conference on Concurrency Theory (CONCUR 2018), vol. 118. Leibniz International Proceedings in Informatics (LIPIcs), Dagstuhl, Germany: Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, 17:1\u201317:17."},{"key":"S0960129523000245_ref6","unstructured":"Bacci, G. , Mardare, R. , Panangaden, P. , and Plotkin, G. (2021). Tensor of quantitative equational theories. In Gadducci, F. and Silva, A. (eds.), 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021), volume 211 of Leibniz International Proceedings in Informatics (LIPIcs), Dagstuhl, Germany: Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, 7:1\u20137:17."},{"key":"S0960129523000245_ref39","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2015.08.002"},{"key":"S0960129523000245_ref46","doi-asserted-by":"crossref","unstructured":"Mitchell, J. C. and Scedrov, A. (1992). Notes on sconing and relators. In Computer Science Logic, 6th Workshop, CSL \u201992, vol. 702. LNCS. Springer, 352\u2013378.","DOI":"10.1007\/3-540-56992-8_21"},{"key":"S0960129523000245_ref5","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785715"},{"key":"S0960129523000245_ref58","doi-asserted-by":"publisher","DOI":"10.1007\/s10958-008-9013-7"},{"key":"S0960129523000245_ref14","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934554"},{"key":"S0960129523000245_ref61","doi-asserted-by":"publisher","DOI":"10.1198\/jasa.2009.tm08651"},{"key":"S0960129523000245_ref11","unstructured":"Barthe, G. , D\u2019Argenio, P. R. , and Rezk, T. (2004). Secure information flow by self-composition. In Proceedings of the 17th IEEE Workshop on Computer Security Foundations, CSFW \u201904, vol. 100, USA: IEEE Computer Society."},{"key":"S0960129523000245_ref62","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68237-0_5"},{"key":"S0960129523000245_ref13","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677000"},{"key":"S0960129523000245_ref3","article-title":"Monads need not be endofunctors","volume":"11","author":"Altenkirch","year":"2015","journal-title":"Logical Methods in Computer Science"},{"key":"S0960129523000245_ref20","doi-asserted-by":"publisher","DOI":"10.1145\/3188745.3188946"},{"key":"S0960129523000245_ref32","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0022272"},{"key":"S0960129523000245_ref21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-53641-4_24"},{"key":"S0960129523000245_ref26","doi-asserted-by":"publisher","DOI":"10.1561\/0400000042"},{"key":"S0960129523000245_ref55","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2014.10.017"},{"key":"S0960129523000245_ref33","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005137"},{"key":"S0960129523000245_ref22","doi-asserted-by":"publisher","DOI":"10.1145\/3093333.3009858"},{"key":"S0960129523000245_ref43","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934518"},{"key":"S0960129523000245_ref51","article-title":"A note on differential privacy: Defining resistance to arbitrary side information","volume":"6","author":"Prasad","year":"2014","journal-title":"Journal of Privacy and Confidentiality"},{"key":"S0960129523000245_ref59","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exab051"},{"key":"S0960129523000245_ref25","doi-asserted-by":"publisher","DOI":"10.1007\/11681878_14"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129523000245","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,11]],"date-time":"2023-09-11T02:06:56Z","timestamp":1694398016000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129523000245\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,4]]},"references-count":62,"journal-issue":{"issue":"4-5","published-print":{"date-parts":[[2023,4]]}},"alternative-id":["S0960129523000245"],"URL":"https:\/\/doi.org\/10.1017\/s0960129523000245","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"type":"print","value":"0960-1295"},{"type":"electronic","value":"1469-8072"}],"subject":[],"published":{"date-parts":[[2023,4]]},"assertion":[{"value":"\u00a9 The Author(s), 2023. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}}]}}