{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,24]],"date-time":"2026-02-24T18:30:21Z","timestamp":1771957821819,"version":"3.50.1"},"reference-count":87,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/V038699\/1"],"award-info":[{"award-number":["EP\/V038699\/1"]}],"id":[{"id":"10.13039\/501100000266","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":[[2024,1,2]]},"abstract":"<jats:p>Rewriting is a principled term transformation technique with uses across theorem proving and compilation. In theorem proving, each rewrite is a proof step; in compilation, rewrites optimize a program term. While developing rewrite sequences manually is possible, this process does not scale to larger rewrite sequences. Automated rewriting techniques, like greedy simplification or equality saturation, work well without requiring human input. Yet, they do not scale to large search spaces, limiting the complexity of tasks where automated rewriting is effective, and meaning that just a small increase in term size or rewrite length may result in failure.<\/jats:p>\n          <jats:p>\n            This paper proposes a semi-automatic rewriting technique as a means to scale rewriting by allowing human insight at key decision points. Specifically, we propose\n            <jats:italic toggle=\"yes\">guided equality saturation<\/jats:italic>\n            that embraces human guidance when fully automated equality saturation does not scale. The rewriting is split into two simpler automatic equality saturation steps: from the original term to a human-provided intermediate\n            <jats:italic toggle=\"yes\">guide<\/jats:italic>\n            , and from the guide to the target. Complex rewriting tasks may require multiple guides, resulting in a sequence of equality saturation steps. A guide can be a complete term, or a\n            <jats:italic toggle=\"yes\">sketch<\/jats:italic>\n            containing undefined elements that are instantiated by the equality saturation search. Such sketches may be far more concise than complete terms.\n          <\/jats:p>\n          <jats:p>We demonstrate the generality and effectiveness of guided equality saturation using two case studies. First, we integrate guided equality saturation in the Lean 4 proof assistant. Proofs are written in the style of textbook proof sketches, as a series of calculations omitting details and skipping steps. These proofs conclude in less than a second instead of minutes when compared to unguided equality saturation, and can find complex proofs that previously had to be done manually. Second, in the compiler of the RISE array language, where unguided equality saturation fails to perform optimizations within an hour and using 60 GB of memory, guided equality saturation performs the same optimizations with at most 3 guides, within seconds using less than 1 GB memory.<\/jats:p>","DOI":"10.1145\/3632900","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T20:48:51Z","timestamp":1704487731000},"page":"1727-1758","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Guided Equality Saturation"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8461-8075","authenticated-orcid":false,"given":"Thomas","family":"K\u0153hler","sequence":"first","affiliation":[{"name":"Inria, Nancy, France"},{"name":"ICube lab - Universit\u00e9 de Strasbourg - CNRS, Strasbourg, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0409-1363","authenticated-orcid":false,"given":"Andr\u00e9s","family":"Goens","sequence":"additional","affiliation":[{"name":"University of Amsterdam, Amsterdam, Netherlands"},{"name":"University of Edinburgh, Edinburgh, United Kingdom"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-6410-3681","authenticated-orcid":false,"given":"Siddharth","family":"Bhat","sequence":"additional","affiliation":[{"name":"University of Edinburgh, Edinburgh, United Kingdom"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3874-6003","authenticated-orcid":false,"given":"Tobias","family":"Grosser","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"},{"name":"University of Edinburgh, Edinburgh, United Kingdom"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0190-7010","authenticated-orcid":false,"given":"Phil","family":"Trinder","sequence":"additional","affiliation":[{"name":"University of Glasgow, Glasgow, United Kingdom"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5048-0741","authenticated-orcid":false,"given":"Michel","family":"Steuwer","sequence":"additional","affiliation":[{"name":"TU Berlin, Berlin, Germany"},{"name":"University of Edinburgh, Edinburgh, United Kingdom"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485486"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485486"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800000988"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139172752"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1093\/LOGCOM\/4.3.217"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3557998"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10817-013-9278-5"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24364-6_2"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14203-1_9"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/10721975_5"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373830"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10817-011-9225-2"},{"key":"e_1_3_2_14_1","unstructured":"Chun Chen Jacqueline Chame and Mary Hall. 2008. CHiLL: A framework for composing high-level loop transformations. Technical Report. Citeseer."},{"key":"e_1_3_2_15_1","first-page":"578","volume-title":"13th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2018, Carlsbad, CA, USA, October 8-10, 2018","author":"Chen Tianqi","year":"2018","unstructured":"Tianqi Chen, Thierry Moreau, Ziheng Jiang, Lianmin Zheng, Eddie Q. Yan, Haichen Shen, Meghan Cowan, Leyuan Wang, Yuwei Hu, Luis Ceze, Carlos Guestrin, and Arvind Krishnamurthy. 2018. TVM: An Automated End-to-End Optimizing Compiler for Deep Learning. In 13th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2018, Carlsbad, CA, USA, October 8-10, 2018, Andrea C. Arpaci-Dusseau and Geoff Voelker (Eds.). USENIX Association, 578\u2013594. https:\/\/www.usenix.org\/conference\/osdi18\/presentation\/chen"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1088149.1088169"},{"key":"e_1_3_2_17_1","first-page":"78","volume-title":"Types for Proofs and Programs, International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers (Lecture Notes in Computer Science, Vol. 4502)","author":"Corbineau Pierre","year":"2006","unstructured":"Pierre Corbineau. 2006. Deciding Equality in the Constructor Theory. In Types for Proofs and Programs, International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers (Lecture Notes in Computer Science, Vol. 4502), Thorsten Altenkirch and Conor McBride (Eds.). Springer. 78\u201392https:\/\/doi.org\/10.1007\/978-3-540-74464-1_6"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/PACT.2017.24"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-79876-5_37"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73595-3-13"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-56883-2_11"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044450813-3\/50018-7"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_7"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9904-1978-14516-9"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.34727\/2022\/ISBN.978-3-85448-053-2_13"},{"key":"e_1_3_2_28_1","unstructured":"Emil Holm Gj\u00f8rup and Bas Spitters. 2020. Congruence closure in cubical type theory. In Workshop on Homotopy Type Theory\/Univalent Foundations. https:\/\/www.cs.au.dk\/\u02dc spitters\/Emil.pdf."},{"issue":"11","key":"e_1_3_2_29_1","first-page":"1382","article-title":"Formal proof\u2013the four-color theorem","volume":"55","author":"Gonthier Georges","year":"2008","unstructured":"Georges Gonthier et al. 2008. Formal proof\u2013the four-color theorem. Notices of the AMS 55, 11 (2008), 1382\u20131393.","journal-title":"Notices of the AMS"},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-09724-4"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408974"},{"key":"e_1_3_2_32_1","first-page":"100","volume-title":"Proceedings of the 2018 International Symposium on Code Generation and Optimization, CGO 2018, V\u00f6sendorf \/ Vienna, Austria, February 24-28, 2018","author":"Hagedorn Bastian","year":"2018","unstructured":"Bastian Hagedorn, Larisa Stoltzfus, Michel Steuwer, Sergei Gorlatch,and Christophe Dubach. 2018. High performance stencil code generation with lift. In Proceedings of the 2018 International Symposium on Code Generation and Optimization, CGO 2018, V\u00f6sendorf \/ Vienna, Austria, February 24-28, 2018, Jens Knoop, Markus Schordan, Teresa Johnson, and Michael F. P. O\u2019Boyle (Eds.). ACM, 100\u2013112.https:\/\/doi.org\/10.1145\/3168824"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.1017\/fmp.2017.1"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(92)90047-7"},{"key":"e_1_3_2_35_1","unstructured":"Joe Hurd. 2003. First-order proof tactics in higher-order logic theorem provers. Design and Application of Strategies\/Tactics in Higher Order Logics number NASA\/CP-2003-212448 in NASA Technical Reports (2003) 56\u201368."},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/VL\/HCC51201.2021.9576341"},{"key":"e_1_3_2_37_1","article-title":"Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs","author":"Qiaochu Jiang Albert","year":"2023","unstructured":"Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Timoth\u00e9e Lacroix, Jiacheng Liu, Wenda Li, Mateja Jamnik, Guillaume Lample, and Yuhuai Wu. 2023. Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs. In The Eleventh International Conference on Learning Representations, ICLR 2023, Kigali, Rwanda, May 1-5, 2023. OpenReview.net. https:\/\/openreview.net\/pdf?id=SMa9EAovKMC","journal-title":"The Eleventh International Conference on Learning Representations, ICLR 2023, Kigali, Rwanda, May 1-5, 2023"},{"key":"e_1_3_2_38_1","first-page":"203","article-title":"Playing by the rules: rewriting as a practical optimisation technique in CHC","volume":"1","author":"Jones Simon Peyton","year":"2001","unstructured":"Simon Peyton Jones, Andrew Tolmach, Tony Hoare. 2001. Playing by the rules: rewriting as a practical optimisation technique in CHC. In Haskell workshop, 1. 203\u2013233","journal-title":"In Haskell workshop"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(77)90002-3"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-81955-1_23"},{"key":"e_1_3_2_41_1","doi-asserted-by":"publisher","DOI":"10.5525\/GLA.THESIS.83323"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/CGO51591.2021.9370337"},{"key":"e_1_3_2_43_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.SCICO.2020.102440"},{"key":"e_1_3_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3497776.3517781"},{"key":"e_1_3_2_45_1","first-page":"19","article-title":"On the Complexity of the Standard Translation of Lambda Calculus into Combinatory Logic","volume":"53","author":"Lachowski Lukasz","year":"2018","unstructured":"Lukasz Lachowski. 2018. On the Complexity of the Standard Translation of Lambda Calculus into Combinatory Logic. Reports Math. Log. 53 (2018), 19\u201342. https:\/\/rml.tcs.uj.edu.pl\/rml-53\/02-lachowski.pdf","journal-title":"Reports Math. Log"},{"key":"e_1_3_2_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/CGO.2004.1281665"},{"key":"e_1_3_2_47_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.SYSARC.2017.06.005"},{"key":"e_1_3_2_48_1","volume-title":"Program synthesis by sketching","author":"Lezama A Solar","year":"2008","unstructured":"A Solar Lezama. 2008. Program synthesis by sketching. Ph.D. Dissertation. PhD thesis, EECS Department, University of California, Berkeley."},{"key":"e_1_3_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3573105.3575671"},{"key":"e_1_3_2_50_1","doi-asserted-by":"publisher","DOI":"10.1109\/PACT.2011.68"},{"key":"e_1_3_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3366428.3380771"},{"key":"e_1_3_2_52_1","doi-asserted-by":"publisher","unstructured":"Ravi Teja Mullapudi Vinay Vasista and Uday Bondhugula. 2015. PolyMage: Automatic Optimization for Image Processing Pipelines. (2015) 429\u2013443. https:\/\/doi.org\/10.1145\/2694344.2694364 10.1145\/2694344.2694364","DOI":"10.1145\/2694344.2694364"},{"key":"e_1_3_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386012"},{"key":"e_1_3_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485496"},{"key":"e_1_3_2_55_1","doi-asserted-by":"publisher","DOI":"10.5555\/909447"},{"key":"e_1_3_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/322186.322198"},{"key":"e_1_3_2_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32033-3_33"},{"key":"e_1_3_2_58_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.IC.2006.08.009"},{"key":"e_1_3_2_59_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0141-9331(02)00011-X"},{"key":"e_1_3_2_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-39185-1_15"},{"key":"e_1_3_2_61_1","doi-asserted-by":"publisher","DOI":"10.1109\/SC.2004.61"},{"key":"e_1_3_2_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74591-4_18"},{"key":"e_1_3_2_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFB0054170"},{"key":"e_1_3_2_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386001"},{"key":"e_1_3_2_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/2185520.2185528"},{"key":"e_1_3_2_66_1","doi-asserted-by":"publisher","unstructured":"Jonathan Ragan-Kelley Connelly Barnes Andrew Adams Sylvain Paris Fr\u00e9do Durand and Saman P. Amarasinghe. 2013. Halide: a language and compiler for optimizing parallelism locality and recomputation in image processing pipelines. (2013) 519\u2013530. https:\/\/doi.org\/10.1145\/2491956.2462176 10.1145\/2491956.2462176","DOI":"10.1145\/2491956.2462176"},{"key":"e_1_3_2_67_1","unstructured":"Alexandre Riazanov and Andrei Voronkov. 1999. Vampire. 1632 (1999) 19990292\u20130292"},{"key":"e_1_3_2_68_1","unstructured":"Joseph J Rotman. 2006. A first course in abstract algebra: with applications."},{"key":"e_1_3_2_69_1","unstructured":"Peter Scholze. 2021. Liquid tensor experiment. Experimental Mathematics (2021) 1\u20136"},{"key":"e_1_3_2_70_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40229-1_8"},{"key":"e_1_3_2_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/3406117"},{"key":"e_1_3_2_72_1","doi-asserted-by":"publisher","unstructured":"Gus Henry Smith Andrew Liu Steven Lyubomirsky Scott Davidson Joseph McMahan Michael B. Taylor Luis Ceze and Zachary Tatlock. 2021. Pure tensor program rewriting via access patterns (representation pearl). (2021) 21\u201331. https:\/\/doi.org\/10.1145\/3460945.3464953 10.1145\/3460945.3464953","DOI":"10.1145\/3460945.3464953"},{"key":"e_1_3_2_73_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781141"},{"key":"e_1_3_2_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784754"},{"key":"e_1_3_2_75_1","unstructured":"Michel Steuwer Thomas Koehler Bastian K\u00f6pcke and Federico Pizzuti. 2022. RISE Shine: Language-Oriented Compiler Design. CoRR abs\/2201.03611 (2022). arXiv:2201.03611 https:\/\/arxiv.org\/abs\/2201.03611"},{"key":"e_1_3_2_76_1","doi-asserted-by":"publisher","DOI":"10.1109\/CGO.2017.7863730"},{"key":"e_1_3_2_77_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480915"},{"key":"e_1_3_2_78_1","doi-asserted-by":"publisher","DOI":"10.1145\/1128022.1128042"},{"key":"e_1_3_2_79_1","doi-asserted-by":"publisher","DOI":"10.1145\/3445814.3446707"},{"key":"e_1_3_2_80_1","doi-asserted-by":"publisher","DOI":"10.1145\/289423.289425"},{"key":"e_1_3_2_81_1","doi-asserted-by":"publisher","DOI":"10.14778\/3407790.3407799"},{"key":"e_1_3_2_82_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02959-2_10"},{"key":"e_1_3_2_83_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24849-1_24"},{"key":"e_1_3_2_84_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434304"},{"key":"e_1_3_2_85_1","doi-asserted-by":"publisher","DOI":"10.1145\/3355089.3356518"},{"key":"e_1_3_2_86_1","author":"Yang Yichen","year":"2021","unstructured":"Yichen Yang, Phitchaya Mangpo Phothilimthana, Yisu Remy Wang, Max Willsey, Sudip Roy, and Jacques Pienaar. 2021. Equality Saturation for Tensor Graph Superoptimization. (2021). https:\/\/proceedings.mlsys.org\/paper\/2021\/hash\/65ded5353c5ee48d0b7d48c591b8f430-Abstract.html","journal-title":"Equality Saturation for Tensor Graph Superoptimization"},{"key":"e_1_3_2_87_1","first-page":"863","volume-title":"14th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2020, Virtual Event, November 4-6, 2020","author":"Zheng Lianmin","year":"2020","unstructured":"Lianmin Zheng, Chengfan Jia, Minmin Sun, Zhao Wu, Cody Hao Yu, Ameer Haj-Ali, Yida Wang, Jun Yang, Danyang Zhuo, Koushik Sen, Joseph E. Gonzalez, and Ion Stoica. 2020. Ansor: Generating High-Performance Tensor Programs for Deep Learning. In 14th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2020, Virtual Event, November 4-6, 2020. USENIX Association, 863\u2013879. https:\/\/www.usenix.org\/conference\/osdi20\/presentation\/zheng"},{"key":"e_1_3_2_88_1","volume-title":"Interactive Program Restructuring. (Restructuration interactive des programmes)","author":"Zinenko Oleksandr","year":"2016","unstructured":"Oleksandr Zinenko. 2016. Interactive Program Restructuring. (Restructuration interactive des programmes). Ph.D. Dissertation. University of Paris-Saclay, France. https:\/\/tel.archives-ouvertes.fr\/tel-01414770"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632900","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632900","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:02:33Z","timestamp":1751659353000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632900"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":87,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632900"],"URL":"https:\/\/doi.org\/10.1145\/3632900","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}