{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:45:49Z","timestamp":1780994749700,"version":"3.54.1"},"reference-count":135,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2024,11,11]],"date-time":"2024-11-11T00:00:00Z","timestamp":1731283200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100003246","name":"Dutch Research Council","doi-asserted-by":"crossref","award":["016.Veni.192.259"],"award-info":[{"award-number":["016.Veni.192.259"]}],"id":[{"id":"10.13039\/501100003246","id-type":"DOI","asserted-by":"crossref"}]},{"name":"Villum Investigator","award":["25804"],"award-info":[{"award-number":["25804"]}]},{"name":"European Union\u2019s Horizon 2020 Framework Programme","award":["683289"],"award-info":[{"award-number":["683289"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2024,12,31]]},"abstract":"<jats:p>\n            Type soundness, which asserts that \u201cwell-typed programs cannot go wrong,\u201d is widely viewed as the canonical theorem one must prove to establish that a type system is doing its job. It is commonly proved using the so-called\n            <jats:italic>syntactic approach<\/jats:italic>\n            (also known as\n            <jats:italic>progress and preservation<\/jats:italic>\n            ), which has had a huge impact on the study and teaching of programming language foundations. Unfortunately, syntactic type soundness is a rather weak theorem. It only applies to programs that are well typed in their entirety and thus tells us nothing about the many programs written in \u201csafe\u201d languages that make use of \u201cunsafe\u201d language features. Even worse, it tells us nothing about whether type systems achieve one of their main goals: enforcement of data abstraction. One can easily define a language that enjoys syntactic type soundness and yet fails to support even the most basic modular reasoning principles for abstraction mechanisms like closures, objects, and abstract data types.\n          <\/jats:p>\n          <jats:p>\n            Given these concerns, we argue that programming languages researchers should no longer be satisfied with proving syntactic type soundness and should instead start proving\n            <jats:italic>semantic type soundness<\/jats:italic>\n            , a more useful theorem that captures more accurately what type systems are actually good for. Semantic type soundness is an old idea\u2014Milner\u2019s original account of type soundness from 1978 was semantic\u2014but it fell out of favor in the 1990s due to limitations and complexities of denotational models. In the succeeding decades, thanks to a series of technical advances\u2014notably,\n            <jats:italic>step-indexed Kripke logical relations<\/jats:italic>\n            constructed over operational semantics and\n            <jats:italic>higher-order concurrent separation logic<\/jats:italic>\n            as consolidated in the\n            <jats:italic>Iris<\/jats:italic>\n            framework in Coq\u2014we can now build (machine-checked) semantic soundness proofs at a much higher level of abstraction than was previously possible.\n          <\/jats:p>\n          <jats:p>\n            The resulting \u201clogical\u201d approach to semantic type soundness has already been employed to great effect in a number of recent papers, but those papers typically (a) concern advanced problem scenarios that complicate the presentation, (b) assume significant prior knowledge of the reader, and (c) suppress many details of the proofs. Here, we aim to provide a gentler, more pedagogically motivated introduction to logical type soundness, targeted at a broader audience that may or may not be familiar with logical relations and Iris. As a bonus, we also show how logical type soundness proofs can easily be generalized to establish an even stronger\n            <jats:italic>relational<\/jats:italic>\n            property\u2014\n            <jats:italic>representation independence<\/jats:italic>\n            \u2014for realistic type systems.\n          <\/jats:p>","DOI":"10.1145\/3676954","type":"journal-article","created":{"date-parts":[[2024,7,10]],"date-time":"2024-07-10T10:58:41Z","timestamp":1720609121000},"page":"1-75","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":31,"title":["A Logical Approach to Type Soundness"],"prefix":"10.1145","volume":"71","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2237-851X","authenticated-orcid":false,"given":"Amin","family":"Timany","sequence":"first","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1185-5237","authenticated-orcid":false,"given":"Robbert","family":"Krebbers","sequence":"additional","affiliation":[{"name":"Radboud University Nijmegen, Nijmegen, Netherlands"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3884-6867","authenticated-orcid":false,"given":"Derek","family":"Dreyer","sequence":"additional","affiliation":[{"name":"MPI-SWS, Saarbr\u00fccken, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1320-0098","authenticated-orcid":false,"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,11,11]]},"reference":[{"key":"e_1_3_3_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1990.113761"},{"key":"e_1_3_3_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/1037736"},{"key":"e_1_3_3_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1709093.1709094"},{"key":"e_1_3_3_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029818"},{"key":"e_1_3_3_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480925"},{"key":"e_1_3_3_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_6"},{"key":"e_1_3_3_8_1","volume-title":"A Non-type-theoretic Semantics for Type-theoretic Language","author":"Allen Stuart","year":"1987","unstructured":"Stuart Allen. 1987. A Non-type-theoretic Semantics for Type-theoretic Language. Ph.D. Dissertation. Cornell University."},{"key":"e_1_3_3_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2001.932501"},{"key":"e_1_3_3_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/325694.325727"},{"key":"e_1_3_3_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"e_1_3_3_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190235"},{"key":"e_1_3_3_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(90)90151-7"},{"key":"e_1_3_3_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837022"},{"key":"e_1_3_3_15_1","series-title":"Studies in Logic and the Foundations of Mathematics","volume-title":"The Lambda Calculus\u2014Its Syntax and Semantics","author":"Barendregt Hendrik Pieter","year":"1985","unstructured":"Hendrik Pieter Barendregt. 1985. The Lambda Calculus\u2014Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics, Vol. 103. North-Holland."},{"key":"e_1_3_3_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/11874683_12"},{"key":"e_1_3_3_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596567"},{"key":"e_1_3_3_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1481861.1481864"},{"key":"e_1_3_3_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1273920.1273922"},{"key":"e_1_3_3_20_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-9(4:4)2013"},{"key":"e_1_3_3_21_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1999.2828"},{"key":"e_1_3_3_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926401"},{"key":"e_1_3_3_23_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2012.107"},{"key":"e_1_3_3_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.07.010"},{"key":"e_1_3_3_25_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129510000162"},{"key":"e_1_3_3_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040327"},{"key":"e_1_3_3_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.034"},{"key":"e_1_3_3_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/143165.143230"},{"key":"e_1_3_3_29_1","volume-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"Constable Robert L.","year":"1986","unstructured":"Robert L. Constable, Stuart F. Allen, Mark Bromley, Rance Cleaveland, J. F. Cremer, Robert Harper, Douglas J. Howe, Todd B. Knoblock, N. P. Mendler, Prakash Panangaden, James T. Sasaki, and Scott F. Smith. 1986. Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall. http:\/\/dl.acm.org\/citation.cfm?id=10510"},{"key":"e_1_3_3_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.02.010"},{"key":"e_1_3_3_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44202-9_9"},{"key":"e_1_3_3_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371102"},{"key":"e_1_3_3_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"e_1_3_3_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30044-8_9"},{"key":"e_1_3_3_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSP.2016.22"},{"key":"e_1_3_3_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_3_3_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429104"},{"key":"e_1_3_3_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14107-2_24"},{"key":"e_1_3_3_39_1","unstructured":"Derek Dreyer. 2018. Milner Award Lecture: The type soundness theorem that you really want to prove (and now you can). Keynote talk at POPL 2018. https:\/\/www.youtube.com\/watch?v=8Xyk_dGcAwk&ab_channel=POPL2018"},{"key":"e_1_3_3_40_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-7(2:16)2011"},{"key":"e_1_3_3_41_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681200024X"},{"key":"e_1_3_3_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706323"},{"key":"e_1_3_3_43_1","unstructured":"Derek Dreyer Simon Spies Lennard G\u00e4her Ralf Jung Jan-Oliver Kaiser Hoang-Hai Dang David Swasey Jan Menz Niklas M\u00fcck and Benjamin Peters. 2022. Semantics of Type Systems (Lecture Notes). Retrieved from https:\/\/plv.mpi-sws.org\/semantics-course\/"},{"key":"e_1_3_3_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90014-7"},{"key":"e_1_3_3_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209174"},{"key":"e_1_3_3_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00003"},{"key":"e_1_3_3_47_1","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-17(3:9)2021"},{"key":"e_1_3_3_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632854"},{"key":"e_1_3_3_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15375-4_27"},{"key":"e_1_3_3_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434287"},{"key":"e_1_3_3_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408996"},{"key":"e_1_3_3_52_1","volume-title":"Interpretation fonctionelle et elimination des coupures de l\u2019arithmetique d\u2019ordre superieur","author":"Girard Jean-Yves","year":"1972","unstructured":"Jean-Yves Girard. 1972. Interpretation fonctionelle et elimination des coupures de l\u2019arithmetique d\u2019ordre superieur. Ph.D. Dissertation. Universite Paris VII."},{"key":"e_1_3_3_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384619"},{"key":"e_1_3_3_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434291"},{"key":"e_1_3_3_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/371880.371887"},{"key":"e_1_3_3_56_1","doi-asserted-by":"publisher","DOI":"10.5555\/3002812"},{"key":"e_1_3_3_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_3_3_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371074"},{"key":"e_1_3_3_59_1","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-18(2:16)2022"},{"key":"e_1_3_3_60_1","doi-asserted-by":"publisher","unstructured":"Jonas Kastberg Hinrichsen Dani\u00ebl Louwrink Robbert Krebbers and Jesper Bengtson. 2021. Machine-checked semantic session typing. (2021) 178\u2013198. 10.1145\/3437992.3439914","DOI":"10.1145\/3437992.3439914"},{"key":"e_1_3_3_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926402"},{"key":"e_1_3_3_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103666"},{"key":"e_1_3_3_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.375719"},{"key":"e_1_3_3_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632889"},{"key":"e_1_3_3_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434288"},{"key":"e_1_3_3_66_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0037110"},{"key":"e_1_3_3_67_1","volume-title":"Understanding and Evolving the Rust Programming Language","author":"Jung Ralf","year":"2020","unstructured":"Ralf Jung. 2020. Understanding and Evolving the Rust Programming Language. Ph.D. Dissertation. Saarland University. https:\/\/publikationen.sulb.uni-saarland.de\/handle\/20.500.11880\/29647"},{"key":"e_1_3_3_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_3_3_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/3418295"},{"key":"e_1_3_3_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951943"},{"key":"e_1_3_3_71_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_3_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371113"},{"key":"e_1_3_3_73_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_3_3_74_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2017.17"},{"key":"e_1_3_3_75_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01220868"},{"key":"e_1_3_3_76_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01304852"},{"key":"e_1_3_3_77_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111050"},{"key":"e_1_3_3_78_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236772"},{"key":"e_1_3_3_79_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_26"},{"key":"e_1_3_3_80_1","doi-asserted-by":"publisher","DOI":"10.1145\/3093333.3009855"},{"key":"e_1_3_3_81_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2011.38"},{"key":"e_1_3_3_82_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364527.2364536"},{"key":"e_1_3_3_83_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(94)90047-7"},{"key":"e_1_3_3_84_1","doi-asserted-by":"publisher","DOI":"10.1145\/3093333.3009877"},{"key":"e_1_3_3_85_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74915-8_23"},{"key":"e_1_3_3_86_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9099-0"},{"key":"e_1_3_3_87_1","doi-asserted-by":"publisher","DOI":"10.1145\/99583.99622"},{"key":"e_1_3_3_88_1","doi-asserted-by":"publisher","DOI":"10.1145\/800055.802036"},{"key":"e_1_3_3_89_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(86)80019-5"},{"key":"e_1_3_3_90_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"e_1_3_3_91_1","doi-asserted-by":"publisher","DOI":"10.1145\/512644.512669"},{"key":"e_1_3_3_92_1","doi-asserted-by":"publisher","DOI":"10.1145\/44501.45065"},{"key":"e_1_3_3_93_1","doi-asserted-by":"publisher","DOI":"10.1145\/224164.224182"},{"key":"e_1_3_3_94_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2019.01.002"},{"key":"e_1_3_3_95_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2000.855774"},{"key":"e_1_3_3_96_1","unstructured":"Emeric Nasi. 2011. Modify Any Java Class Field Using Reflection. Retrieved from https:\/\/blog.sevagas.com\/Modify-any-Java-class-field-using-reflection"},{"key":"e_1_3_3_97_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596572"},{"key":"e_1_3_3_98_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784764"},{"key":"e_1_3_3_99_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"e_1_3_3_100_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44802-0_1"},{"key":"e_1_3_3_101_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511525902.013"},{"key":"e_1_3_3_102_1","doi-asserted-by":"publisher","DOI":"10.5555\/509043"},{"key":"e_1_3_3_103_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0052"},{"key":"e_1_3_3_104_1","first-page":"245","volume-title":"Advanced Topics in Types and Programming Languages","author":"Pitts Andrew M.","year":"2005","unstructured":"Andrew M. Pitts. 2005. Typed operational reasoning. In Advanced Topics in Types and Programming Languages, B. C. Pierce (Ed.). The MIT Press, 245\u2013289."},{"key":"e_1_3_3_105_1","volume-title":"HOOTS","author":"Pitts Andrew M.","year":"1998","unstructured":"Andrew M. Pitts and Ian Stark. 1998. Operational reasoning for functions with local state. In HOOTS."},{"key":"e_1_3_3_106_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0037118"},{"key":"e_1_3_3_107_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591265"},{"key":"e_1_3_3_108_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-06859-7_148"},{"key":"e_1_3_3_109_1","first-page":"513","volume-title":"Information Processing 83","author":"Reynolds John C.","year":"1983","unstructured":"John C. Reynolds. 1983. Types, abstraction and parametric polymorphism. In Information Processing 83. 513\u2013523."},{"key":"e_1_3_3_110_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_3_3_111_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796814000264"},{"key":"e_1_3_3_112_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371100"},{"key":"e_1_3_3_113_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454036"},{"key":"e_1_3_3_114_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129512000035"},{"key":"e_1_3_3_115_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454031"},{"key":"e_1_3_3_116_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547631"},{"key":"e_1_3_3_117_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190244"},{"key":"e_1_3_3_118_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04027-6_33"},{"key":"e_1_3_3_119_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.09.009"},{"key":"e_1_3_3_120_1","doi-asserted-by":"publisher","DOI":"10.1145\/1284320.1284325"},{"key":"e_1_3_3_121_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_9"},{"key":"e_1_3_3_122_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_11"},{"key":"e_1_3_3_123_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133913"},{"key":"e_1_3_3_124_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1046"},{"key":"e_1_3_3_125_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_34"},{"key":"e_1_3_3_126_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034831"},{"key":"e_1_3_3_127_1","volume-title":"Contributions in Programming Languages Theory","author":"Timany Amin","year":"2018","unstructured":"Amin Timany. 2018. Contributions in Programming Languages Theory. Ph.D. Dissertation. KU Leuven. https:\/\/lirias.kuleuven.be\/retrieve\/510052"},{"key":"e_1_3_3_128_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341709"},{"key":"e_1_3_3_129_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632862"},{"key":"e_1_3_3_130_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158152"},{"key":"e_1_3_3_131_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(90)90018-D"},{"key":"e_1_3_3_132_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500600"},{"key":"e_1_3_3_133_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429111"},{"key":"e_1_3_3_134_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01018828"},{"key":"e_1_3_3_135_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"},{"key":"e_1_3_3_136_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.036"}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3676954","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3676954","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:19:12Z","timestamp":1750295952000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3676954"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,11]]},"references-count":135,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2024,12,31]]}},"alternative-id":["10.1145\/3676954"],"URL":"https:\/\/doi.org\/10.1145\/3676954","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"value":"0004-5411","type":"print"},{"value":"1557-735X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,11,11]]},"assertion":[{"value":"2022-11-23","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-06-11","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-11","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}