{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:22:11Z","timestamp":1751660531417,"version":"3.41.0"},"reference-count":88,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T00:00:00Z","timestamp":1641945600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-sa\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["818616"],"award-info":[{"award-number":["818616"]}],"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":[[2022,1,16]]},"abstract":"<jats:p>\n            Semantics is traditionally concerned with program equivalence, in which all pairs of programs which are\n            <jats:italic>not<\/jats:italic>\n            equivalent are treated the same, and simply dubbed as incomparable. In recent years, various forms of program\n            <jats:italic>metrics<\/jats:italic>\n            have been introduced such that the distance between non-equivalent programs is measured as an element of an appropriate quantale. By letting the underlying quantale\n            <jats:italic>vary<\/jats:italic>\n            as the type of the compared programs become more complex, the recently introduced framework of differential logical relations allows for a new contextual form of reasoning. In this paper, we show that all this can be generalised to\n            <jats:italic>effectful<\/jats:italic>\n            higher-order programs, in which not only the\n            <jats:italic>values<\/jats:italic>\n            , but also the\n            <jats:italic>effects<\/jats:italic>\n            computations produce can be appropriately distanced in a principled way. We show that the resulting framework is flexible, allowing various forms of effects to be handled, and that it provides compact and informative judgments about program differences.\n          <\/jats:p>","DOI":"10.1145\/3498680","type":"journal-article","created":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T17:03:12Z","timestamp":1642006992000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Effectful program distancing"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9200-070X","authenticated-orcid":false,"given":"Ugo","family":"Dal Lago","sequence":"first","affiliation":[{"name":"University of Bologna, Italy \/ Inria, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Francesco","family":"Gavazzo","sequence":"additional","affiliation":[{"name":"University of Bologna, Italy \/ Inria, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,1,12]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90082-5"},{"key":"e_1_2_2_2_1","volume-title":"Sussman","author":"Abelson Harold","year":"1996","unstructured":"Harold Abelson and Gerald J . Sussman . 1996 . Structure and Interpretation of Computer Programs, Second Edition . MIT Press . Harold Abelson and Gerald J. Sussman. 1996. Structure and Interpretation of Computer Programs, Second Edition. MIT Press."},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796819000145"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17127-8_3"},{"key":"e_1_2_2_5_1","volume-title":"Hoogendijk","author":"Backhouse Roland Carl","year":"1993","unstructured":"Roland Carl Backhouse and Paul F . Hoogendijk . 1993 . Elements of a Relational Theory of Datatypes. In Formal Program Development - IFIP TC2\/WG 2.1 State-of-the-Art Report . 7\u201342. Roland Carl Backhouse and Paul F. Hoogendijk. 1993. Elements of a Relational Theory of Datatypes. In Formal Program Development - IFIP TC2\/WG 2.1 State-of-the-Art Report. 7\u201342."},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-14(3:20)2018"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0060439"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158145"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2014.36"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677000"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934554"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2492061"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964003"},{"key":"e_1_2_2_14_1","volume-title":"Bird and Oege de Moor","author":"Richard","year":"1997","unstructured":"Richard S. Bird and Oege de Moor . 1997 . Algebra of programming. Prentice Hall . Richard S. Bird and Oege de Moor. 1997. Algebra of programming. Prentice Hall."},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814301"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594304"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254086"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509546"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44584-6_4"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706308"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2025113.2025131"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009858"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:APCS.0000018144.87456.10"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2015.64"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_13"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_10"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2019.09.007"},{"key":"e_1_2_2_28_1","volume-title":"Proc. of ICTCS","author":"Lago Ugo Dal","year":"2020","unstructured":"Ugo Dal Lago and Francesco Gavazzo . 2020 . Differential Logical Relations Part II: Increments and Derivatives . In Proc. of ICTCS 2020. 101\u2013114. Ugo Dal Lago and Francesco Gavazzo. 2020. Differential Logical Relations Part II: Increments and Derivatives. In Proc. of ICTCS 2020. 101\u2013114."},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2021.09.027"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2021.23"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498692"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005117"},{"key":"e_1_2_2_33_1","volume-title":"Proc. of ICTCS","author":"Lago Ugo Dal","year":"2017","unstructured":"Ugo Dal Lago , Francesco Gavazzo , and Ryo Tanaka . 2017 . Effectful Applicative Similarity for Call-by-Name Lambda Calculi . In Proc. of ICTCS 2017. 87\u201398. Ugo Dal Lago, Francesco Gavazzo, and Ryo Tanaka. 2017. Effectful Applicative Similarity for Call-by-Name Lambda Calculi. In Proc. of ICTCS 2017. 87\u201398."},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2019.12.025"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ICALP.2019.111"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535872"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2505351.2505353"},{"key":"e_1_2_2_38_1","unstructured":"B.A. Davey and H.A. Priestley. 1990. Introduction to lattices and order. Cambridge University Press.  B.A. Davey and H.A. Priestley. 1990. Introduction to lattices and order. Cambridge University Press."},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009890"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785715"},{"volume-title":"Semantics of Probabilistic Processes: An Operational Approach","author":"Deng Y.","key":"e_1_2_2_41_1","unstructured":"Y. Deng . 2015. Semantics of Probabilistic Processes: An Operational Approach . Springer Berlin Heidelberg . Y. Deng. 2015. Semantics of Probabilistic Processes: An Operational Approach. Springer Berlin Heidelberg."},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2003.09.013"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-47677-3_5"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/146370.146381"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(97)00236-3"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429113"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209149"},{"volume-title":"Coinductive Equivalences and Metrics for Higher-order Languages with Algebraic Effects. Ph. D. Dissertation","author":"Gavazzo Francesco","key":"e_1_2_2_48_1","unstructured":"Francesco Gavazzo . 2019. Coinductive Equivalences and Metrics for Higher-order Languages with Algebraic Effects. Ph. D. Dissertation . University of Bologna , Italy. http:\/\/amsdottorato.unibo.it\/9075\/ Francesco Gavazzo. 2019. Coinductive Equivalences and Metrics for Higher-order Languages with Algebraic Effects. Ph. D. Dissertation. University of Bologna, Italy. http:\/\/amsdottorato.unibo.it\/9075\/"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-12(4:12)2016"},{"volume-title":"Optimizing and incrementalizing higher-order collection queries by AST transformation. Ph. D. Dissertation","author":"Giarrusso P.G.","key":"e_1_2_2_50_1","unstructured":"P.G. Giarrusso . 2018. Optimizing and incrementalizing higher-order collection queries by AST transformation. Ph. D. Dissertation . University of T\u00fcbingen. P.G. Giarrusso. 2018. Optimizing and incrementalizing higher-order collection queries by AST transformation. Ph. D. Dissertation. University of T\u00fcbingen."},{"volume-title":"Practical Foundations for Programming Languages (2nd. Ed.)","author":"Harper Robert","key":"e_1_2_2_51_1","unstructured":"Robert Harper . 2016. Practical Foundations for Programming Languages (2nd. Ed.) . Cambridge University Press . Robert Harper. 2016. Practical Foundations for Programming Languages (2nd. Ed.). Cambridge University Press."},{"key":"e_1_2_2_52_1","first-page":"113","article-title":"A cottage industry of lax extensions","volume":"3","author":"Hoffman D.","year":"2015","unstructured":"D. Hoffman . 2015 . A cottage industry of lax extensions . Categories and General Algebraic Structures with Applications , 3 , 1 (2015), 113 \u2013 151 . D. Hoffman. 2015. A cottage industry of lax extensions. Categories and General Algebraic Structures with Applications, 3, 1 (2015), 113\u2013151.","journal-title":"Categories and General Algebraic Structures with Applications"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.aim.2007.04.013"},{"volume-title":"A Categorical Approach to Order, Metric, and Topology","author":"Topology Monoidal","key":"e_1_2_2_54_1","unstructured":"2014. Monoidal Topology . A Categorical Approach to Order, Metric, and Topology , D. Hofmann, G.J. Seal, and W. Tholen (Eds.) (Encyclopedia of Mathematics and its Applications). Cambridge University Press . 2014. Monoidal Topology. A Categorical Approach to Order, Metric, and Topology, D. Hofmann, G.J. Seal, and W. Tholen (Eds.) (Encyclopedia of Mathematics and its Applications). Cambridge University Press."},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-14(4:6)2018"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2015.08.002"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75307"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02924844"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00088-9"},{"volume-title":"Categories for the Working Mathematician","author":"MacLane S.","key":"e_1_2_2_60_1","unstructured":"S. MacLane . 1971. Categories for the Working Mathematician . Springer-Verlag . S. MacLane. 1971. Categories for the Working Mathematician. Springer-Verlag."},{"key":"e_1_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00415-1"},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-23702-7_24"},{"key":"e_1_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/2893356"},{"key":"e_1_2_2_64_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1989.39155"},{"key":"e_1_2_2_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250790.1250803"},{"key":"e_1_2_2_66_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470696"},{"volume-title":"Lambda-Definability and Logical Relations. Memorandum SAI-RM-4","author":"Plotkin Gordon D.","key":"e_1_2_2_67_1","unstructured":"Gordon D. Plotkin . 1973. Lambda-Definability and Logical Relations. Memorandum SAI-RM-4 , University of Edinburgh Gordon D. Plotkin. 1973. Lambda-Definability and Logical Relations. Memorandum SAI-RM-4, University of Edinburgh"},{"key":"e_1_2_2_68_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45315-6_1"},{"key":"e_1_2_2_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341696"},{"key":"e_1_2_2_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158124"},{"key":"e_1_2_2_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/158511.158710"},{"key":"e_1_2_2_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863568"},{"volume-title":"An Introduction to the Calculus of Finite Differences","author":"Richardson C.H.","key":"e_1_2_2_73_1","unstructured":"C.H. Richardson . 1954. An Introduction to the Calculus of Finite Differences . New York . C.H. Richardson. 1954. An Introduction to the Calculus of Finite Differences. New York."},{"key":"e_1_2_2_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/1929501.1929517"},{"key":"e_1_2_2_75_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993518"},{"key":"e_1_2_2_76_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594294"},{"volume-title":"Higher Order Operational Techniques in Semantics","author":"Sands D.","key":"e_1_2_2_77_1","unstructured":"D. Sands . 1998. Improvement Theory and Its Applications . In Higher Order Operational Techniques in Semantics , A. D. Gordon and A. M. Pitts (Eds.). Cambridge University Press , 275\u2013306. D. Sands. 1998. Improvement Theory and Its Applications. In Higher Order Operational Techniques in Semantics, A. D. Gordon and A. M. Pitts (Eds.). Cambridge University Press, 275\u2013306."},{"key":"e_1_2_2_78_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785668"},{"key":"e_1_2_2_79_1","unstructured":"R. Sedgewick and P. Flajolet. 2013. An Introduction to the Analysis of Algorithms. Pearson Education.  R. Sedgewick and P. Flajolet. 2013. An Introduction to the Analysis of Algorithms. Pearson Education."},{"key":"e_1_2_2_80_1","doi-asserted-by":"publisher","DOI":"10.1145\/2025113.2025133"},{"key":"e_1_2_2_81_1","doi-asserted-by":"publisher","DOI":"10.1214\/aoms\/1177700153"},{"key":"e_1_2_2_82_1","unstructured":"A.M. Thijs. 1996. Simulation and fixpoint semantics. Rijksuniversiteit Groningen.  A.M. Thijs. 1996. Simulation and fixpoint semantics. Rijksuniversiteit Groningen."},{"key":"e_1_2_2_83_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.09.035"},{"volume-title":"Optimal Transport: Old and New","author":"Villani C.","key":"e_1_2_2_84_1","unstructured":"C. Villani . 2008. Optimal Transport: Old and New . Springer Berlin Heidelberg . C. Villani. 2008. Optimal Transport: Old and New. Springer Berlin Heidelberg."},{"key":"e_1_2_2_85_1","volume-title":"Westbrook and Swarat Chaudhuri","author":"Edwin","year":"2013","unstructured":"Edwin M. Westbrook and Swarat Chaudhuri . 2013 . A Semantics for Approximate Program Transformations. CoRR , abs\/1304.5531 (2013), arxiv:1304.5531 Edwin M. Westbrook and Swarat Chaudhuri. 2013. A Semantics for Approximate Program Transformations. CoRR, abs\/1304.5531 (2013), arxiv:1304.5531"},{"key":"e_1_2_2_86_1","doi-asserted-by":"publisher","DOI":"10.1145\/2593069.2593156"},{"key":"e_1_2_2_87_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341697"},{"key":"e_1_2_2_88_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35632-2_26"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498680","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3498680","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:30:28Z","timestamp":1750188628000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498680"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1,12]]},"references-count":88,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2022,1,16]]}},"alternative-id":["10.1145\/3498680"],"URL":"https:\/\/doi.org\/10.1145\/3498680","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2022,1,12]]},"assertion":[{"value":"2022-01-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}