{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:11:56Z","timestamp":1775873516384,"version":"3.50.1"},"reference-count":74,"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\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["CCF-1901381"],"award-info":[{"award-number":["CCF-1901381"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"publisher","award":["MURI FA9550-15-1-0053, FA9550-19- 1-0216, and FA9550-21-0009"],"award-info":[{"award-number":["MURI FA9550-15-1-0053, FA9550-19- 1-0216, and FA9550-21-0009"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100006602","name":"Air Force Research Laboratory","doi-asserted-by":"publisher","award":["NDSEG fellowship"],"award-info":[{"award-number":["NDSEG fellowship"]}],"id":[{"id":"10.13039\/100006602","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            We present\n            <jats:bold>calf<\/jats:bold>\n            , a\n            <jats:bold>c<\/jats:bold>\n            ost-\n            <jats:bold>a<\/jats:bold>\n            ware\n            <jats:bold>l<\/jats:bold>\n            ogical\n            <jats:bold>f<\/jats:bold>\n            ramework for studying quantitative aspects of functional programs. Taking inspiration from recent work that reconstructs traditional aspects of programming languages in terms of a modal account of\n            <jats:italic>phase distinctions<\/jats:italic>\n            , we argue that the cost structure of programs motivates a phase distinction between\n            <jats:italic>intension<\/jats:italic>\n            and\n            <jats:italic>extension<\/jats:italic>\n            . Armed with this technology, we contribute a synthetic account of cost structure as a computational effect in which cost-aware programs enjoy an internal noninterference property: input\/output behavior cannot depend on cost. As a full-spectrum dependent type theory,\n            <jats:bold>calf<\/jats:bold>\n            presents a unified language for programming and specification of both cost and behavior that can be integrated smoothly with existing mathematical libraries available in type theoretic proof assistants.\n          <\/jats:p>\n          <jats:p>\n            We evaluate\n            <jats:bold>calf<\/jats:bold>\n            as a general framework for cost analysis by implementing two fundamental techniques for algorithm analysis: the\n            <jats:italic>method of recurrence relations<\/jats:italic>\n            and\n            <jats:italic>physicist\u2019s method for amortized analysis<\/jats:italic>\n            . We deploy these techniques on a variety of case studies: we prove a tight, closed bound for Euclid\u2019s algorithm, verify the amortized complexity of batched queues, and derive tight, closed bounds for the sequential and\n            <jats:italic>parallel<\/jats:italic>\n            complexity of merge sort, all fully mechanized in the Agda proof assistant. Lastly we substantiate the soundness of quantitative reasoning in\n            <jats:bold>calf<\/jats:bold>\n            by means of a model construction.\n          <\/jats:p>","DOI":"10.1145\/3498670","type":"journal-article","created":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T17:03:12Z","timestamp":1642006992000},"page":"1-31","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":19,"title":["A cost-aware logical framework"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4888-6042","authenticated-orcid":false,"given":"Yue","family":"Niu","sequence":"first","affiliation":[{"name":"Carnegie Mellon University, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0585-5564","authenticated-orcid":false,"given":"Jonathan","family":"Sterling","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0947-3520","authenticated-orcid":false,"given":"Harrison","family":"Grodin","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9400-2941","authenticated-orcid":false,"given":"Robert","family":"Harper","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}]}],"member":"320","published-online":{"date-parts":[[2022,1,12]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"Blelloch","author":"Acar Umut A.","year":"2019","unstructured":"Umut A. Acar and Guy E . Blelloch . 2019 . Algorithms : Parallel and Sequential . http:www.algorithms-book.com Umut A. Acar and Guy E. Blelloch. 2019. Algorithms: Parallel and Sequential. http:www.algorithms-book.com"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2016.6"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837638"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1017\/9781108854429.007"},{"key":"e_1_2_2_5_1","volume-title":"Amortised Resource Analysis with Separation Logic","author":"Atkey Robert","year":"1957","unstructured":"Robert Atkey . 2010. Amortised Resource Analysis with Separation Logic . In Programming Languages and Systems, Andrew D. Gordon (Ed.). Springer Berlin Heidelberg , Berlin, Heidelberg . 85\u2013103. isbn:978-3-642-1 1957 -6 Robert Atkey. 2010. Amortised Resource Analysis with Separation Logic. In Programming Languages and Systems, Andrew D. Gordon (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 85\u2013103. isbn:978-3-642-11957-6"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2011.16"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49630-5_2"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/224164.224210"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/232627.232650"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129505004822"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681300018X"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(82)90015-1"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373830"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-1(2:1)2005"},{"key":"e_1_2_2_15_1","volume-title":"Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant","author":"Chlipala Adam","unstructured":"Adam Chlipala . 2013. Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant . The MIT Press . isbn:0-262-02665-1 Adam Chlipala. 2013. Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant. The MIT Press. isbn:0-262-02665-1"},{"key":"e_1_2_2_16_1","unstructured":"R. L. Constable S. F. Allen H. M. Bromley W. R. Cleaveland J. F. Cremer R. W. Harper D. J. Howe T. B. Knoblock N. P. Mendler P. Panangaden J. T. Sasaki and S. F. Smith. 1986. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall Inc. Upper Saddle River NJ USA. isbn:0-13-451832-2  R. L. Constable S. F. Allen H. M. Bromley W. R. Cleaveland J. F. Cremer R. W. Harper D. J. Howe T. B. Knoblock N. P. Mendler P. Panangaden J. T. Sasaki and S. F. Smith. 1986. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall Inc. Upper Saddle River NJ USA. isbn:0-13-451832-2"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1017\/9781316755983.009"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/357233.357238"},{"key":"e_1_2_2_19_1","unstructured":"The Coq Development Team. 2016. The Coq Proof Assistant Reference Manual.  The Coq Development Team. 2016. The Coq Proof Assistant Reference Manual."},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2019.01.015"},{"key":"e_1_2_2_21_1","volume-title":"Introduction to Algorithms","author":"Cormen Thomas H.","unstructured":"Thomas H. Cormen , Charles E. Leiserson , Ronald L. Rivest , and Clifford Stein . 2009. Introduction to Algorithms , 3 rd Edition. MIT Press . isbn:978-0-262-03384-8 http:\/\/mitpress.mit.edu\/books\/introduction-algorithms Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. 2009. Introduction to Algorithms, 3rd Edition. MIT Press. isbn:978-0-262-03384-8 http:\/\/mitpress.mit.edu\/books\/introduction-algorithms","edition":"3"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/325694.325716"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328457"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784749"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236786"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209146"},{"key":"e_1_2_2_27_1","volume-title":"Rast: A Language for Resource-Aware Session Types. CoRR, abs\/2012.13129","author":"Das Ankush","year":"2020","unstructured":"Ankush Das and Frank Pfenning . 2020 . Rast: A Language for Resource-Aware Session Types. CoRR, abs\/2012.13129 (2020), Dec., arxiv:2012.13129 Submitted . Ankush Das and Frank Pfenning. 2020. Rast: A Language for Resource-Aware Session Types. CoRR, abs\/2012.13129 (2020), Dec., arxiv:2012.13129 Submitted."},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/382780.382785"},{"key":"e_1_2_2_29_1","unstructured":"Manuel Eberl. 2015. The Akra-Bazzi theorem and the Master theorem. Archive of Formal Proofs July issn:2150-914x https:\/\/isa-afp.org\/entries\/Akra_Bazzi.html  Manuel Eberl. 2015. The Akra-Bazzi theorem and the Master theorem. Archive of Formal Proofs July issn:2150-914x https:\/\/isa-afp.org\/entries\/Akra_Bazzi.html"},{"key":"e_1_2_2_30_1","unstructured":"Manuel Eberl. 2017. The Median-of-Medians Selection Algorithm. Archive of Formal Proofs Dec. issn:2150-914x https:\/\/isa-afp.org\/entries\/Median_Of_Medians_Selection.html  Manuel Eberl. 2017. The Median-of-Medians Selection Algorithm. Archive of Formal Proofs Dec. issn:2150-914x https:\/\/isa-afp.org\/entries\/Median_Of_Medians_Selection.html"},{"key":"e_1_2_2_31_1","unstructured":"Manuel Eberl. 2017. The number of comparisons in QuickSort. Archive of Formal Proofs March issn:2150-914x https:\/\/isa-afp.org\/entries\/Quick_Sort_Cost.html  Manuel Eberl. 2017. The number of comparisons in QuickSort. Archive of Formal Proofs March issn:2150-914x https:\/\/isa-afp.org\/entries\/Quick_Sort_Cost.html"},{"key":"e_1_2_2_32_1","doi-asserted-by":"crossref","unstructured":"Marcelo P. Fiore Andrew M. Pitts and S. C. Steenkamp. 2021. Quotients inductive types and quotient inductive types. arXiv:2101.02994.  Marcelo P. Fiore Andrew M. Pitts and S. C. Steenkamp. 2021. Quotients inductive types and quotient inductive types. arXiv:2101.02994.","DOI":"10.46298\/lmcs-18(2:15)2022"},{"key":"e_1_2_2_33_1","volume-title":"Formal Proof \u2014 The Four-Color Theorem. Notices of the AMS, 55, 11","author":"Gonthier G.","year":"2008","unstructured":"G. Gonthier . 2008. Formal Proof \u2014 The Four-Color Theorem. Notices of the AMS, 55, 11 ( 2008 ), https:\/\/www.ams.org\/notices\/200811\/tx081101382p.pdf G. Gonthier. 2008. Formal Proof \u2014 The Four-Color Theorem. Notices of the AMS, 55, 11 (2008), https:\/\/www.ams.org\/notices\/200811\/tx081101382p.pdf"},{"key":"e_1_2_2_34_1","unstructured":"Daniel Gratzer and Jonathan Sterling. 2020. Syntactic categories for dependent type theory: sketching and adequacy. arXiv:2012.10783.  Daniel Gratzer and Jonathan Sterling. 2020. Syntactic categories for dependent type theory: sketching and adequacy. arXiv:2012.10783."},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/316686.316690"},{"key":"e_1_2_2_36_1","volume-title":"The Science of Programming","author":"Gries David","unstructured":"David Gries . 1987. The Science of Programming ( 1 st ed.). Springer-Verlag, Berlin , Heidelberg . isbn:0-387-96480-0 David Gries. 1987. The Science of Programming (1st ed.). Springer-Verlag, Berlin, Heidelberg. isbn:0-387-96480-0","edition":"1"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373826"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371092"},{"key":"e_1_2_2_39_1","unstructured":"Robert Harper. 2018. PFPL Supplement: Types and Parallelism. https:\/\/www.cs.cmu.edu\/~rwh\/pfpl\/supplements\/par.pdf  Robert Harper. 2018. PFPL Supplement: Types and Parallelism. https:\/\/www.cs.cmu.edu\/~rwh\/pfpl\/supplements\/par.pdf"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/96709.96744"},{"key":"e_1_2_2_41_1","volume-title":"Resource Aware ML","author":"Hoffmann Jan","unstructured":"Jan Hoffmann , Klaus Aehlig , and Martin Hofmann . 2012. Resource Aware ML . In Computer Aided Verification, P. Madhusudan and Sanjit A. Seshia (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg . 781\u2013786. isbn:978-3-642-31424-7 Jan Hoffmann, Klaus Aehlig, and Martin Hofmann. 2012. Resource Aware ML. In Computer Aided Verification, P. Madhusudan and Sanjit A. Seshia (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 781\u2013786. isbn:978-3-642-31424-7"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46425-5_11"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604148"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(81)90030-2"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706327"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005089"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371083"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.2307\/1990131"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190245"},{"key":"e_1_2_2_54_1","volume-title":"V. 2)","author":"Levy Paul Blain","unstructured":"Paul Blain Levy . 2004. Call-By-Push-Value : A Functional\/Imperative Synthesis (Semantics Structures in Computation , V. 2) . Kluwer Academic Publishers, Norwell, MA , USA. isbn:1-4020-1730-8 Paul Blain Levy. 2004. Call-By-Push-Value: A Functional\/Imperative Synthesis (Semantics Structures in Computation, V. 2). Kluwer Academic Publishers, Norwell, MA, USA. isbn:1-4020-1730-8"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-006-0480-6"},{"key":"e_1_2_2_56_1","volume-title":"Time Credits and Time Receipts in Iris","author":"M\u00e9vel Glen","unstructured":"Glen M\u00e9vel , Jacques-Henri Jourdan , and Fran\u00e7ois Pottier . 2019. Time Credits and Time Receipts in Iris . In Programming Languages and Systems, Lu\u00eds Caires (Ed.). Springer International Publishing , Cham . 3\u201329. isbn:978-3-030-17184-1 Glen M\u00e9vel, Jacques-Henri Jourdan, and Fran\u00e7ois Pottier. 2019. Time Credits and Time Receipts in Iris. In Programming Languages and Systems, Lu\u00eds Caires (Ed.). Springer International Publishing, Cham. 3\u201329. isbn:978-3-030-17184-1"},{"key":"e_1_2_2_57_1","volume-title":"Peter Lammich, Christian Sternagel, Simon Wimmer, and Bohua Zhan.","author":"Nipkow Tobias","year":"2021","unstructured":"Tobias Nipkow , Jasmin Blanchette , Manuel Eberl , Alejandro G\u00f3mez Londo\u00f1o , Peter Lammich, Christian Sternagel, Simon Wimmer, and Bohua Zhan. 2021 . Functional Algorithms , Verified!. https:\/\/functional-algorithms-verified.org Tobias Nipkow, Jasmin Blanchette, Manuel Eberl, Alejandro G\u00f3mez Londo\u00f1o, Peter Lammich, Christian Sternagel, Simon Wimmer, and Bohua Zhan. 2021. Functional Algorithms, Verified!. https:\/\/functional-algorithms-verified.org"},{"key":"e_1_2_2_58_1","unstructured":"Yue Niu and Robert Harper. 2020. Cost-Aware Type Theory. arXiv:2011.03660.  Yue Niu and Robert Harper. 2020. Cost-Aware Type Theory. arXiv:2011.03660."},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/3462303"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04652-0_5"},{"key":"e_1_2_2_61_1","volume-title":"Purely Functional Data Structures","author":"Okasaki Chris","unstructured":"Chris Okasaki . 1998. Purely Functional Data Structures . Cambridge University Press , USA. isbn:0-521-63124-6 Chris Okasaki. 1998. Purely Functional Data Structures. Cambridge University Press, USA. isbn:0-521-63124-6"},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2015.12.020"},{"key":"e_1_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371126"},{"key":"e_1_2_2_64_1","doi-asserted-by":"publisher","DOI":"10.5555\/871816.871845"},{"key":"e_1_2_2_65_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(77)90044-5"},{"key":"e_1_2_2_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434308"},{"key":"e_1_2_2_67_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-16(1:2)2020"},{"key":"e_1_2_2_68_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-00704-1"},{"key":"e_1_2_2_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411240"},{"key":"e_1_2_2_70_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470719"},{"key":"e_1_2_2_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/3474834"},{"key":"e_1_2_2_72_1","volume-title":"Verified Functional Programming in Agda","author":"Stump Aaron","unstructured":"Aaron Stump . 2016. Verified Functional Programming in Agda . Association for Computing Machinery and Morgan & Claypool . isbn:978-1-970001-27-3 Aaron Stump. 2016. Verified Functional Programming in Agda. Association for Computing Machinery and Morgan & Claypool. isbn:978-1-970001-27-3"},{"key":"e_1_2_2_73_1","doi-asserted-by":"publisher","DOI":"10.1137\/0606031"},{"key":"e_1_2_2_74_1","unstructured":"Taichi Uemura. 2019. A General Framework for the Semantics of Type Theory. arXiv:1904.04097.  Taichi Uemura. 2019. A General Framework for the Semantics of Type Theory. arXiv:1904.04097."},{"key":"e_1_2_2_75_1","unstructured":"Sebastian Andreas Ullrich. 2016. Simple Verification of Rust Programs via Functional Purification. Master\u2019s thesis. IPD Snelting.  Sebastian Andreas Ullrich. 2016. Simple Verification of Rust Programs via Functional Purification. Master\u2019s thesis. IPD Snelting."},{"key":"e_1_2_2_76_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133903"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498670","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3498670","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3498670","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:30:27Z","timestamp":1750188627000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498670"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1,12]]},"references-count":74,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2022,1,16]]}},"alternative-id":["10.1145\/3498670"],"URL":"https:\/\/doi.org\/10.1145\/3498670","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"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"}}]}}