{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:42:29Z","timestamp":1780994549812,"version":"3.54.1"},"reference-count":47,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2021,8,19]],"date-time":"2021-08-19T00:00:00Z","timestamp":1629331200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001691","name":"Japan Society for the Promotion of Science","doi-asserted-by":"publisher","award":["20K19775"],"award-info":[{"award-number":["20K19775"]}],"id":[{"id":"10.13039\/501100001691","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002241","name":"Japan Science and Technology Agency","doi-asserted-by":"publisher","award":["JPM-JER1603"],"award-info":[{"award-number":["JPM-JER1603"]}],"id":[{"id":"10.13039\/501100002241","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["CCF-2040222, CCF-1718220"],"award-info":[{"award-number":["CCF-2040222, CCF-1718220"]}],"id":[{"id":"10.13039\/100000001","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,8,22]]},"abstract":"<jats:p>Adversarial computations are a widely studied class of computations where resource-bounded probabilistic adversaries have access to oracles, i.e., probabilistic procedures with private state. These computations arise routinely in several domains, including security, privacy and machine learning.<\/jats:p>\n          <jats:p>In this paper, we develop program logics for reasoning about adversarial computations in a higher-order setting. Our logics are built on top of a simply typed \u03bb-calculus extended with a graded monad for probabilities and state. The grading is used to model and restrict the memory footprint and the cost (in terms of oracle calls) of computations. Under this view, an adversary is a higher-order expression that expects as arguments the code of its oracles. We develop unary program logics for reasoning about error probabilities and expected values, and a relational logic for reasoning about coupling-based properties. All logics feature rules for adversarial computations, and yield guarantees that are valid for all adversaries that satisfy a fixed resource policy. We prove the soundness of the logics in the category of quasi-Borel spaces, using a general notion of graded predicate liftings, and we use logical relations over graded predicate liftings to establish the soundness of proof rules for adversaries. We illustrate the working of our logics with simple but illustrative examples.<\/jats:p>","DOI":"10.1145\/3473598","type":"journal-article","created":{"date-parts":[[2021,8,19]],"date-time":"2021-08-19T10:44:29Z","timestamp":1629369869000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["Higher-order probabilistic adversarial computations: categorical semantics and program logics"],"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":"Aarhus University, Denmark"}],"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"}]},{"given":"Marco","family":"Gaboardi","sequence":"additional","affiliation":[{"name":"Boston University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0888-3093","authenticated-orcid":false,"given":"Deepak","family":"Garg","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7529-5489","authenticated-orcid":false,"given":"Shin-ya","family":"Katsumata","sequence":"additional","affiliation":[{"name":"National Institute of Informatics, Japan"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9895-9209","authenticated-orcid":false,"given":"Tetsuya","family":"Sato","sequence":"additional","affiliation":[{"name":"Tokyo Institute of Technology, Japan"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2021,8,19]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110265"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434333"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2020.09.002"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1215\/ijm\/1255631584"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1866307.1866350"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158145"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978391"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2578855.2535847"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ICALP.2016.107"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480894"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54792-8_8"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103670"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535869"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46678-0_18"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/362686.362692"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03332-3_9"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3319535.3354235"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2015.64"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2011.02.001"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSP.2016.22"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1561\/0400000042"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2010.08.005"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSN.2015.21"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005137"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/73007.73012"},{"key":"e_1_2_2_27_1","volume-title":"A Programming Language","author":"Iverson Kenneth E.","unstructured":"Kenneth E. Iverson . 1962. A Programming Language . John Wiley & Sons, Inc. , USA. isbn:0471430145 Kenneth E. Iverson. 1962. A Programming Language. John Wiley & Sons, Inc., USA. isbn:0471430145"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2015.38"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_15"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535846"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-14(4:6)2018"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/800061.808758"},{"key":"e_1_2_2_34_1","volume-title":"Categories for the Working Mathematician","author":"MacLane Saunders","unstructured":"Saunders MacLane . 1971. Categories for the Working Mathematician . Springer-Verlag , New York . Graduate Texts in Mathematics, Vol. 5 . Saunders MacLane. 1971. Categories for the Working Mathematician. Springer-Verlag, New York. Graduate Texts in Mathematics, Vol. 5."},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371072"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17127-8_22"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/229542.229547"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491522.2491523"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006953"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3306193"},{"key":"e_1_2_2_41_1","volume-title":"Higher Order Operational Techniques in Semantics","author":"Pitts Andrew","unstructured":"Andrew Pitts and Ian Stark . 1998. Operational Reasoning for Functions with Local State . In Higher Order Operational Techniques in Semantics , Andrew Gordon and Andrew Pitts (Eds.). Publications of the Newton Institute, Cambridge University Press , 227\u2013273. http:\/\/www.inf.ed.ac.uk\/~stark\/operfl.html Andrew Pitts and Ian Stark. 1998. Operational Reasoning for Functions with Local State. In Higher Order Operational Techniques in Semantics, Andrew Gordon and Andrew Pitts (Eds.). Publications of the Newton Institute, Cambridge University Press, 227\u2013273. http:\/\/www.inf.ed.ac.uk\/~stark\/operfl.html"},{"key":"e_1_2_2_42_1","unstructured":"Gordon Plotkin. 1973. Lambda-definability and logical relations.  Gordon Plotkin. 1973. Lambda-definability and logical relations."},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20465-4_27"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2016.09.043"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290351"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158148"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290377"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290349"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3473598","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3473598","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3473598","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:28:16Z","timestamp":1750195696000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3473598"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,8,19]]},"references-count":47,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2021,8,22]]}},"alternative-id":["10.1145\/3473598"],"URL":"https:\/\/doi.org\/10.1145\/3473598","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,8,19]]},"assertion":[{"value":"2021-08-19","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}