{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:41:25Z","timestamp":1780994485106,"version":"3.54.1"},"reference-count":112,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T00:00:00Z","timestamp":1736208000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,1,7]]},"abstract":"<jats:p>\n                    Symbolic automata are finite state automata that support potentially infinite alphabets, such as the set of rational numbers, generally applied to regular expressions and languages over finite words. In symbolic automata (or automata modulo \ud835\udc9c), an alphabet is represented by an effective Boolean algebra \ud835\udc9c, supported by a decision procedure for satisfiability. Regular languages over infinite words (so called\n                    <jats:italic toggle=\"yes\">\u03c9<\/jats:italic>\n                    -regular languages) have a rich history paralleling that of regular languages over finite words, with well known applications to model checking via B\u00fcchi automata and temporal logics.\n                  <\/jats:p>\n                  <jats:p>\n                    We generalize symbolic automata to support\n                    <jats:italic toggle=\"yes\">\u03c9<\/jats:italic>\n                    -regular languages via\n                    <jats:italic toggle=\"yes\">transition terms<\/jats:italic>\n                    and\n                    <jats:italic toggle=\"yes\">symbolic derivatives<\/jats:italic>\n                    , bringing together a variety of classic automata and logics in a unified framework that provides all the necessary ingredients to support symbolic model checking modulo \ud835\udc9c. In particular, we define: (1) alternating B\u00fcchi automata modulo \ud835\udc9c(\n                    <jats:italic toggle=\"yes\">AB<\/jats:italic>\n                    <jats:italic toggle=\"yes\">W<\/jats:italic>\n                    <jats:sub>\ud835\udc9c<\/jats:sub>\n                    ) as well (non-alternating) nondeterministic B\u00fcchi automata modulo \ud835\udc9c(\n                    <jats:italic toggle=\"yes\">NB<\/jats:italic>\n                    <jats:italic toggle=\"yes\">W<\/jats:italic>\n                    <jats:sub>\ud835\udc9c<\/jats:sub>\n                    );(2) an alternation elimination algorithm \u00c6 that incrementally constructs an\n                    <jats:italic toggle=\"yes\">NB<\/jats:italic>\n                    <jats:italic toggle=\"yes\">W<\/jats:italic>\n                    <jats:sub>\ud835\udc9c<\/jats:sub>\n                    from an\n                    <jats:italic toggle=\"yes\">AB<\/jats:italic>\n                    <jats:italic toggle=\"yes\">W<\/jats:italic>\n                    <jats:sub>\ud835\udc9c<\/jats:sub>\n                    , and can also be used for constructing the product of two\n                    <jats:italic toggle=\"yes\">NB<\/jats:italic>\n                    <jats:italic toggle=\"yes\">W<\/jats:italic>\n                    <jats:sub>\ud835\udc9c<\/jats:sub>\n                    ; (3) a definition of linear temporal logic modulo \ud835\udc9c,\n                    <jats:bold>LTL<\/jats:bold>\n                    \u27e8\ud835\udc9c\u27e9, that generalizes Vardi's construction of alternating B\u00fcchi automata from LTL, using (2) to go from LTL modulo \ud835\udc9c to\n                    <jats:italic toggle=\"yes\">NB<\/jats:italic>\n                    <jats:italic toggle=\"yes\">W<\/jats:italic>\n                    <jats:sub>\ud835\udc9c<\/jats:sub>\n                    via\n                    <jats:italic toggle=\"yes\">AB<\/jats:italic>\n                    <jats:italic toggle=\"yes\">W<\/jats:italic>\n                    <jats:sub>\ud835\udc9c<\/jats:sub>\n                    .\n                  <\/jats:p>\n                  <jats:p>\n                    Finally, we present\n                    <jats:bold>RLTL<\/jats:bold>\n                    \u27e8 \ud835\udc9c \u27e9, a combination of\n                    <jats:bold>LTL<\/jats:bold>\n                    \u27e8 \ud835\udc9c \u27e9 with extended regular expressions modulo \ud835\udc9c that generalizes the Property Specification Language (PSL). Our combination allows regex\n                    <jats:italic toggle=\"yes\">complement<\/jats:italic>\n                    , that is not supported in PSL but can be supported naturally by using transition terms. We formalize the semantics of\n                    <jats:bold>RLTL<\/jats:bold>\n                    \u27e8 \ud835\udc9c \u27e9 using the\n                    <jats:italic toggle=\"yes\">Lean<\/jats:italic>\n                    proof assistant and formally establish correctness of the main derivation theorem.\n                  <\/jats:p>","DOI":"10.1145\/3704838","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"33-66","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Symbolic Automata: Omega-Regularity Modulo Theories"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-8427-7977","authenticated-orcid":false,"given":"Margus","family":"Veanes","sequence":"first","affiliation":[{"name":"Microsoft Research, Redmond, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9468-5420","authenticated-orcid":false,"given":"Thomas","family":"Ball","sequence":"additional","affiliation":[{"name":"Microsoft Research, Redmond, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4057-9574","authenticated-orcid":false,"given":"Gabriel","family":"Ebner","sequence":"additional","affiliation":[{"name":"Microsoft Research, Redmond, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-8818-5042","authenticated-orcid":false,"given":"Ekaterina","family":"Zhuchko","sequence":"additional","affiliation":[{"name":"Tallinn University of Technology, Tallinn, Estonia"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_14"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-59042-0_96"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(95)80010-7"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46002-0_21"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1051\/ita\/2021008"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43613-4_17"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_8"},{"key":"e_1_3_2_9_1","volume-title":"Principles of Model Checking","author":"Baier Christel","year":"2008","unstructured":"Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking. MIT Press, Cambridge, MA, USA. https:\/\/mitpress.mit.edu\/9780262026499\/principles-of-model-checking\/"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-51803-7_22"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.29007\/1xjt"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-45332-8_18"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48683-6_21"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14162-1_7"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2480359.2429124"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/321239.321249"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(09)70564-6"},{"key":"e_1_3_2_19_1","unstructured":"Doron Bustan Dana Fisman and John Havlicek. 2005. Automata construction for PSL. Technical Report Report MCS05-04. The Weizmann Institute of Science. https:\/\/api.semanticscholar.org\/CorpusID:14807945"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/635499.635502"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(74)80051-6"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2008.2003303"},{"key":"e_1_3_2_23_1","volume-title":"Model Checking","author":"Clarke Edmund M.","year":"1999","unstructured":"Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. 1999. Model Checking. MIT Press, Cambridge, MA, USA. https:\/\/mitpress.mit.edu\/9780262032704\/model-checking\/"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-19992-9_13"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00121128"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48119-2_16"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535849"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2933578"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54577-5_30"},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3093333.3009844"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3419404"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1995376.1995394"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","unstructured":"St\u00e9phane Demri. 2006. Linear-time temporal logics with Presburger constraints: an overview. Journal of Applied Non-Classical Logics16 3-4(2006) 311-347. https:\/\/doi.org\/10.3166\/jancl.16.311-347 10.3166\/jancl.16.311-347","DOI":"10.3166\/jancl.16.311-347"},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2006.09.006"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-25150-9_3"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_4"},{"key":"e_1_3_2_38_1","unstructured":"Alexandre Duret-Lutz. 2024. Spot: a platform for LTL and \u03c9-automata manipulation. https:\/\/spot.lre.epita.fr"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13188-2_9"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-36123-9"},{"key":"e_1_3_2_41_1","doi-asserted-by":"publisher","DOI":"10.5555\/114891.114907"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-16078-7_62"},{"key":"e_1_3_2_43_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90036-0"},{"key":"e_1_3_2_44_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539703420675"},{"key":"e_1_3_2_45_1","doi-asserted-by":"publisher","DOI":"10.29007\/wpg3"},{"key":"e_1_3_2_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_22"},{"key":"e_1_3_2_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99253-8_17"},{"key":"e_1_3_2_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_35"},{"key":"e_1_3_2_49_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.53"},{"key":"e_1_3_2_50_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(79)90046-1"},{"key":"e_1_3_2_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45089-0_5"},{"key":"e_1_3_2_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36206-1_15"},{"key":"e_1_3_2_53_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.01.016"},{"key":"e_1_3_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/567446.567462"},{"key":"e_1_3_2_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44585-4_6"},{"key":"e_1_3_2_56_1","doi-asserted-by":"publisher","unstructured":"Luca Geatti Alessandro Gianola and Nicola Gigante. 2022. Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version). https:\/\/doi.org\/10.48550\/ARXIV.2204.13693 10.48550\/ARXIV.2204.13693","DOI":"10.48550\/ARXIV.2204.13693"},{"key":"e_1_3_2_57_1","first-page":"3","volume-title":"Protocol Specification, Testing and Verification XV, Proceedings of the Fifteenth IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification (Sitges, Spain)","author":"Gerth Rob","year":"1995","unstructured":"Rob Gerth, Doron Peled, Moshe Y. Vardi, and Pierre Wolper. 1995. Simple on-the-fly automatic verification of linear temporal logic. In Protocol Specification, Testing and Verification XV, Proceedings of the Fifteenth IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification (Sitges, Spain), Piotr Dembinski and Marek Sredniawa (Eds.). Chapman & Hall, GBR, 3\u201318. https:\/\/dl.acm.org\/doi\/10.5555\/645837.670574"},{"key":"e_1_3_2_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33386-6_11"},{"key":"e_1_3_2_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-02444-8_28"},{"key":"e_1_3_2_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45657-0_51"},{"key":"e_1_3_2_61_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2001.989799"},{"key":"e_1_3_2_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/3704888"},{"key":"e_1_3_2_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60630-0_5"},{"key":"e_1_3_2_64_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-01090-4_7"},{"key":"e_1_3_2_65_1","doi-asserted-by":"publisher","DOI":"10.5555\/891883"},{"key":"e_1_3_2_66_1","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(85)90074-8"},{"key":"e_1_3_2_67_1","doi-asserted-by":"publisher","DOI":"10.1142\/S012905410200128X"},{"key":"e_1_3_2_68_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_4"},{"key":"e_1_3_2_69_1","first-page":"25","volume-title":"Tenth Annual IEEE Symposium on Logic in Computer Science (LICS\u201995)","author":"Kupferman Orna","year":"1995","unstructured":"Orna Kupferman and Amir Pnueli. 1995. Once and for all. In Tenth Annual IEEE Symposium on Logic in Computer Science (LICS\u201995) (San Diego, CA, USA). IEEE, Piscataway, NJ, USA, 25\u201335. https:\/\/dl.acm.org\/doi\/10.5555\/788017.788753"},{"key":"e_1_3_2_70_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2011.08.006"},{"key":"e_1_3_2_71_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20674-0_6"},{"key":"e_1_3_2_72_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(87)90036-5"},{"key":"e_1_3_2_73_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664573"},{"key":"e_1_3_2_74_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIME.2010.20"},{"key":"e_1_3_2_75_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-15648-8_16"},{"key":"e_1_3_2_76_1","doi-asserted-by":"publisher","DOI":"10.1145\/2480359.2429079"},{"key":"e_1_3_2_77_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(66)80013-X"},{"key":"e_1_3_2_78_1","unstructured":"Microsoft. 2023. App Configuration. https:\/\/azure.microsoft.com\/en- us\/products\/app-configuration\/"},{"key":"e_1_3_2_79_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(84)90049-5"},{"key":"e_1_3_2_80_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591262"},{"key":"e_1_3_2_81_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-16761-7_77"},{"key":"e_1_3_2_82_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1988.5139"},{"key":"e_1_3_2_83_1","doi-asserted-by":"publisher","DOI":"10.1137\/0216062"},{"key":"e_1_3_2_84_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_2"},{"key":"e_1_3_2_85_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_3_2_86_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-82453-1_5"},{"key":"e_1_3_2_87_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0035790"},{"key":"e_1_3_2_88_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71929-3"},{"key":"e_1_3_2_89_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37709-9_15"},{"key":"e_1_3_2_90_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-40965-6_17"},{"key":"e_1_3_2_91_1","doi-asserted-by":"publisher","DOI":"10.1002\/j.1538-7305.1949.tb03624.x"},{"key":"e_1_3_2_92_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90008-9"},{"key":"e_1_3_2_93_1","unstructured":"SMT-LIB. 2021. https:\/\/smtlib.cs.uiowa.edu\/"},{"key":"e_1_3_2_94_1","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_21"},{"key":"e_1_3_2_95_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37703-7_12"},{"key":"e_1_3_2_96_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454066"},{"key":"e_1_3_2_97_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-02508-3_2"},{"key":"e_1_3_2_98_1","doi-asserted-by":"publisher","DOI":"10.1016\/B978-0-444-88074-1.50009-3"},{"key":"e_1_3_2_99_1","unstructured":"Vincent Tourneur and Alexandre Duret-Lutz. 2017. Fixes for two equations in The Blow-Up in Translating LTL to Deterministic Automata by Kupferman and Rosenberg. The original authors have reviewed the fixes and agreed with them."},{"key":"e_1_3_2_100_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-91384-7_2"},{"key":"e_1_3_2_101_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2006.49"},{"key":"e_1_3_2_102_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57887-0_116"},{"key":"e_1_3_2_103_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60915-6_6"},{"key":"e_1_3_2_104_1","first-page":"332","volume-title":"Proceedings of the Symposium on Logic in Computer Science (LICS\u201986) (Cambridge, MA, USA)","author":"Vardi Moshe Y.","year":"1986","unstructured":"Moshe Y. Vardi and Pierre Wolper. 1986. An Automata-Theoretic Approach to Automatic Program Verification (Preliminary Report). In Proceedings of the Symposium on Logic in Computer Science (LICS\u201986) (Cambridge, MA, USA). IEEE, Piscataway, NJ, USA, 332\u2013344. https:\/\/api.semanticscholar.org\/CorpusID:38567081"},{"key":"e_1_3_2_105_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1092"},{"key":"e_1_3_2_106_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2010.15"},{"key":"e_1_3_2_107_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1981.44"},{"key":"e_1_3_2_108_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(83)80051-5"},{"key":"e_1_3_2_109_1","first-page":"119","article-title":"The tableau method for temporal logic: an overview","volume":"28","author":"Wolper Pierre","year":"1985","unstructured":"Pierre Wolper. 1985. The tableau method for temporal logic: an overview. Logique Et Analyse 28 (1985), 119\u2013136. https:\/\/api.semanticscholar.org\/CorpusID:118632087","journal-title":"Logique Et Analyse"},{"key":"e_1_3_2_110_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_6"},{"key":"e_1_3_2_111_1","unstructured":"Ekaterina Zhuchko. 2024. Lean4 Formalization of RLTL. https:\/\/github.com\/ezhuchko\/RLTL-derivatives"},{"key":"e_1_3_2_112_1","doi-asserted-by":"publisher","unstructured":"Ekaterina Zhuchko and Gabriel Ebner. 2024. Artifact for this paper. https:\/\/doi.org\/10.5281\/zenodo.14092718 10.5281\/zenodo.14092718","DOI":"10.5281\/zenodo.14092718"},{"key":"e_1_3_2_113_1","doi-asserted-by":"publisher","DOI":"10.1145\/3636501.3636959"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704838","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704838","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:19:06Z","timestamp":1770200346000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704838"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":112,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704838"],"URL":"https:\/\/doi.org\/10.1145\/3704838","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-08","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-07","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}