{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,23]],"date-time":"2026-03-23T09:59:41Z","timestamp":1774259981154,"version":"3.50.1"},"reference-count":79,"publisher":"Association for Computing Machinery (ACM)","issue":"1","funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"crossref","award":["61902240 and 61902240"],"award-info":[{"award-number":["61902240 and 61902240"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2026,3,31]]},"abstract":"<jats:p>\n                    A desired but challenging property of compiler verification is compositionality, in the sense that the compilation correctness of a program can be deduced incrementally from that of its substructures ranging from statements, functions, and modules. This article proposes a novel compiler verification framework based on denotational semantics for better compositionality, compared to previous approaches based on small-step operational semantics and simulation theories. Our denotational semantics is defined by semantic functions that map a syntactic component to a semantic domain composed of multiple behavioral\n                    <jats:italic toggle=\"yes\">sets<\/jats:italic>\n                    , with compiler correctness established through behavior refinement between the semantic domains of the source and target programs. The main contributions of this article include proposing a denotational semantics for open modules, a novel semantic linking operator, and a refinement algebra that unifies various behavior refinements, making compiler verification structured and compositional. Furthermore, our formalization captures the full meaning of a program and bridges the gap between traditional power-domain-based denotational semantics and the practical needs of compiler verification. We apply our denotation-based framework to verify the front-end of CompCert and typical optimizations on simple prototypes of imperative languages. Our results demonstrate that the compositionality from sub-statements to statements, from functions to modules, and from modules to the whole program can be effectively achieved.\n                  <\/jats:p>","DOI":"10.1145\/3797874","type":"journal-article","created":{"date-parts":[[2026,3,2]],"date-time":"2026-03-02T13:10:31Z","timestamp":1772457031000},"page":"1-65","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Denotation-based Compositional Compiler Verification"],"prefix":"10.1145","volume":"48","author":[{"ORCID":"https:\/\/orcid.org\/0009-0005-3833-6612","authenticated-orcid":false,"given":"Zhang","family":"Cheng","sequence":"first","affiliation":[{"name":"Shanghai Jiao Tong University, Shanghai, China"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-6638-4839","authenticated-orcid":false,"given":"Jiyang","family":"Wu","sequence":"additional","affiliation":[{"name":"Shanghai Jiao Tong University, Shanghai, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2418-7987","authenticated-orcid":false,"given":"Di","family":"Wang","sequence":"additional","affiliation":[{"name":"Peking University, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5678-6538","authenticated-orcid":false,"given":"Qinxiang","family":"Cao","sequence":"additional","affiliation":[{"name":"Shanghai Jiao Tong University, Shanghai, China"}]}],"member":"320","published-online":{"date-parts":[[2026,3,23]]},"reference":[{"key":"e_1_3_3_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90224-P"},{"key":"e_1_3_3_3_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881"},{"key":"e_1_3_3_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.SCICO.2020.102492"},{"key":"e_1_3_3_5_1","first-page":"479","volume-title":"International Colloquium on Automata, Languages, and Programming","author":"Krzysztof R. Apt","year":"1981","unstructured":"R. AptKrzysztofand Gordon D. Plotkin. 1981. A Cook\u2019s tour of countable nondeterminism. In International Colloquium on Automata, Languages, and Programming. Springer, 479\u2013494."},{"key":"e_1_3_3_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(83)90055-5"},{"key":"e_1_3_3_7_1","doi-asserted-by":"publisher","unstructured":"Ralph-Johan Back and Joakim von Wright. 1998. Refinement Calculus\u2014A Systematic Introduction. Springer. DOI: 10.1007\/978-1-4612-1674-2","DOI":"10.1007\/978-1-4612-1674-2"},{"key":"e_1_3_3_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371075"},{"key":"e_1_3_3_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_5"},{"key":"e_1_3_3_10_1","first-page":"328","volume-title":"31st IEEE Computer Security Foundations Symposium (CSF \u201918). IEEE Computer Society","author":"Barthe Gilles","year":"2018","unstructured":"Gilles Barthe, Benjamin Gr\u00e9goire, and Vincent Laporte. 2018b. Secure compilation of side-channel countermeasures: The case of cryptographic \"constant-time\". In 31st IEEE Computer Security Foundations Symposium (CSF \u201918). IEEE Computer Society, 328\u2013343. DOI: 10.1109\/CSF.2018.00031"},{"key":"e_1_3_3_11_1","doi-asserted-by":"crossref","first-page":"30","DOI":"10.1007\/BFb0048939","volume-title":"Programming Languages and Their Definition\u2014Hans Bekic (1936\u20131982)","volume":"177","year":"1984","unstructured":"Hans Beki\u0107. 1984. Definable operation in general algebras, and the theory of automata and flowcharts. In Programming Languages and Their Definition\u2014Hans Bekic (1936\u20131982). Cliff B. Jones (Ed.). Lecture Notes in Computer Science, Vol. 177, Springer, 30\u201355. DOI: 10.1007\/BFB0048939"},{"key":"e_1_3_3_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_7"},{"key":"e_1_3_3_13_1","first-page":"460","volume-title":"Formal Methods, 14th International Symposium on Formal Methods (FM \u201906)","volume":"4085","author":"Blazy Sandrine","year":"2006","unstructured":"Sandrine Blazy, Zaynah Dargaye, and Xavier Leroy. 2006. Formal verification of a C compiler front-end. In Formal Methods, 14th International Symposium on Formal Methods (FM \u201906). Jayadev Misra, Tobias Nipkow, and Emil Sekerinski (Eds.), Lecture Notes in Computer Science, Vol. 4085, Springer, 460\u2013475. DOI: 10.1007\/11813040_31"},{"key":"e_1_3_3_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/828.833"},{"key":"e_1_3_3_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0014683"},{"key":"e_1_3_3_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/321239.321249"},{"key":"e_1_3_3_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10817-018-9457-5"},{"key":"e_1_3_3_18_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.400.6"},{"key":"e_1_3_3_19_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796825100105"},{"key":"e_1_3_3_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571254"},{"key":"e_1_3_3_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3579834"},{"key":"e_1_3_3_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622857"},{"key":"e_1_3_3_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(79)90006-0"},{"key":"e_1_3_3_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632854"},{"key":"e_1_3_3_25_1","first-page":"595","volume-title":"42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL \u201915)","author":"Gu Ronghui","year":"2015","unstructured":"Ronghui Gu, J\u00e9r\u00e9mie Koenig, Tahina Ramananandro, Zhong Shao, Xiongnan (Newman) Wu, Shu-Chun Weng, Haozhong Zhang, and Yu Guo. 2015. Deep specifications and certified abstraction layers. In 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL \u201915). Sriram K. Rajamani and David Walker (Eds.), ACM, New York, NY, 595\u2013608. DOI: 10.1145\/2676726.2676975"},{"key":"e_1_3_3_26_1","first-page":"97","volume-title":"4th International Seminar RelMiCS on Participants Copies for Relational Methods in Logic, Algebra and Computer Science","author":"He Jifeng","year":"1998","unstructured":"Jifeng He and C. A. R. Hoare. 1998. Unifying theories of programming. In 4th International Seminar RelMiCS on Participants Copies for Relational Methods in Logic, Algebra and Computer Science. Ewa Orlowska and Andrzej Szalas (Eds.), 97\u201399."},{"key":"e_1_3_3_27_1","unstructured":"Chung-Kil Hur Georg Neis Derek Dreyer and Viktor Vafeiadis. 2012. The Transitive Composability of Relation Transition Systems. Technical Report MPI-SWS-2012-002 MPI-SWS."},{"key":"e_1_3_3_28_1","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1145\/3314221.3314595","volume-title":"40th ACM SIGPLAN Conference on Programming Language Design and Implementation, (PLDI \u201919)","author":"Jiang Hanru","year":"2019","unstructured":"Hanru Jiang, Hongjin Liang, Siyang Xiao, Junpeng Zha, and Xinyu Feng. 2019. Towards certified separate compilation for concurrent programs. In 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, (PLDI \u201919). Kathryn S. McKinley and Kathleen Fisher (Eds.), ACM, New York, NY, 111\u2013125. DOI: 10.1145\/3314221.3314595"},{"key":"e_1_3_3_29_1","unstructured":"Jacques-Henri Jourdan. 2016. Verasco: A Formally Verified C Static Analyzer (Verasco: Un Analyseur Statique pour C Formellement V\u00e9rifi\u00e9). Ph.\u2009D. Dissertation. Paris Diderot University France. Retrieved from https:\/\/tel.archives-ouvertes.fr\/tel-01327023"},{"key":"e_1_3_3_30_1","first-page":"471","volume-title":"6th IFIP Congress on Information Processing","year":"1974","unstructured":"Gilles Kahn. 1974. The semantics of a simple language for parallel programming. In 6th IFIP Congress on Information Processing. Jack L. Rosenfeld (Ed.), North-Holland, 471\u2013475."},{"key":"e_1_3_3_31_1","doi-asserted-by":"crossref","first-page":"178","DOI":"10.1145\/2837614.2837642","volume-title":"43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL \u201916)","author":"Kang Jeehoon","year":"2016","unstructured":"Jeehoon Kang, Yoonseung Kim, Chung-Kil Hur, Derek Dreyer, and Viktor Vafeiadis. 2016. Lightweight verification of separate compilation. In 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL \u201916). Rastislav Bod\u00edk and Rupak Majumdar (Eds.), ACM, New York, NY, 178\u2013190. DOI: 10.1145\/2837614.2837642"},{"key":"e_1_3_3_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFB0026423"},{"key":"e_1_3_3_33_1","first-page":"1095","volume-title":"42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI \u201921),","author":"Koenig J\u00e9r\u00e9mie","year":"2021","unstructured":"J\u00e9r\u00e9mie Koenig and Zhong Shao. 2021. CompCertO: compiling certified open C components. In 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI \u201921), Stephen N. Freund and Eran Yahav (Eds.), ACM, New York, NY, 1095\u20131109. DOI: 10.1145\/3453483.3454097"},{"key":"e_1_3_3_34_1","first-page":"214","volume-title":"Conference Record of the 5th Annual ACM Symposium on Principles of Programming Languages. Alfred V. Aho, Stephen N. Zilles, and Thomas G. Szymanski (ACM, New York, NY","author":"Kosinki Paul R.","year":"1978","unstructured":"Paul R. Kosinki. 1978. A straightforward denotational semantics for non-determinant data flow programs. In Conference Record of the 5th Annual ACM Symposium on Principles of Programming Languages. Alfred V. Aho, Stephen N. Zilles, and Thomas G. Szymanski (Eds.), ACM, New York, NY, 214\u2013221. DOI: 10.1145\/512760.512783"},{"key":"e_1_3_3_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/256167.256195"},{"key":"e_1_3_3_36_1","unstructured":"Dexter Kozen. 1998. Typed Kleene Algebra. Technical Report. Cornell University."},{"key":"e_1_3_3_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10817-011-9223-4"},{"key":"e_1_3_3_38_1","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1145\/2535838.2535841","volume-title":"41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL \u201914)","author":"Kumar Ramana","year":"2014","unstructured":"Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Scott Owens. 2014. CakeML: A verified implementation of ML. In 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL \u201914). Suresh Jagannathan and Peter Sewell (Eds.), ACM, New York, NY, 179\u2013192. DOI: 10.1145\/2535838.2535841"},{"key":"e_1_3_3_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3492545"},{"key":"e_1_3_3_40_1","first-page":"278","volume-title":"and28th ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation. Jeanne Ferrante and Kathryn S. McKinley (","author":"Lattner Chris","year":"2007","unstructured":"Chris Lattner, Andrew Lenharth, and Vikram S. Adve. 2007. Making context-sensitive points-to analysis with heap cloning practical for the real world. In 28th ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation. Jeanne Ferrante and Kathryn S. McKinley (Eds.), ACM, New York, NY, 278\u2013289. DOI: 10.1145\/1250734.1250766"},{"key":"e_1_3_3_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_3_3_42_1","unstructured":"Xavier Leroy Andrew W. Appel Sandrine Blazy and Gordon Stewart. 2012. The CompCert Memory Model Version 2. Research Report RR-7987. INRIA. Retrieved from http:\/\/hal.inria.fr\/hal-00703441"},{"key":"e_1_3_3_43_1","unstructured":"Xavier Leroy and INRIA. 2024. The CompCert Verified Compiler. Retrieved October 24 2024 from https:\/\/compcert.org\/."},{"key":"e_1_3_3_44_1","first-page":"85","volume-title":"International Symposium on Memory Management (ISMM \u201913)","author":"Li Lian","year":"2013","unstructured":"Lian Li, Cristina Cifuentes, and Nathan Keynes. 2013. Precise and scalable context-sensitive pointer analysis via value flow graph. In International Symposium on Memory Management (ISMM \u201913). Perry Cheng and Erez Petrank (Eds.), ACM, New York, NY, 85\u201396. DOI: 10.1145\/2491894.2466483"},{"key":"e_1_3_3_45_1","doi-asserted-by":"crossref","first-page":"455","DOI":"10.1145\/2103656.2103711","volume-title":"39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL \u201912)","author":"Liang Hongjin","year":"2012","unstructured":"Hongjin Liang, Xinyu Feng, and Ming Fu. 2012. A rely-guarantee-based simulation for verifying concurrent program transformations. In 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL \u201912). John Field and Michael Hicks (Eds.), ACM, New York, NY, 455\u2013468. DOI: 10.1145\/2103656.2103711"},{"key":"e_1_3_3_46_1","doi-asserted-by":"publisher","DOI":"10.1006\/INCO.1995.1134"},{"key":"e_1_3_3_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33314-9_7"},{"key":"e_1_3_3_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/44501.44503"},{"key":"e_1_3_3_49_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90011-6"},{"key":"e_1_3_3_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFB0058037"},{"key":"e_1_3_3_51_1","doi-asserted-by":"crossref","first-page":"166","DOI":"10.1145\/2784731.2784764","volume-title":"Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming (ICFP \u201915)","author":"Neis Georg","year":"2015","unstructured":"Georg Neis, Chung-Kil Hur, Jan-Oliver Kaiser, Craig McLaughlin, Derek Dreyer, and Viktor Vafeiadis. 2015. Pilsner: A compositionally verified compiler for a higher-order imperative language. In Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming (ICFP \u201915). Kathleen Fisher and John H. Reppy (Eds.), ACM, New York, NY, 166\u2013178. DOI: 10.1145\/2784731.2784764"},{"key":"e_1_3_3_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08970-6_29"},{"key":"e_1_3_3_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473591"},{"key":"e_1_3_3_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-10007-5_47"},{"key":"e_1_3_3_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341689"},{"key":"e_1_3_3_56_1","first-page":"383","volume-title":"A constructive denotational semantics for Kahn networks in Coq. From Semantics to Computer Science: Essays in Honour of Gilles Kahn","year":"2009","unstructured":"Christine Paulin-Mohring. 2009. A constructive denotational semantics for Kahn networks in Coq. From Semantics to Computer Science: Essays in Honour of Gilles Kahn. Y. Bertot, G. Huet, J.-J. L\u00e9vy, and G. Plotkin, (Eds.), Cambridge University Press, 383\u2013413."},{"key":"e_1_3_3_57_1","volume-title":"Domains","year":"1983","unstructured":"Gordon Plotkin. 1983. Domains. University of Edinburgh."},{"key":"e_1_3_3_58_1","doi-asserted-by":"publisher","DOI":"10.1137\/0205035"},{"key":"e_1_3_3_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428235"},{"key":"e_1_3_3_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_15"},{"key":"e_1_3_3_61_1","doi-asserted-by":"crossref","first-page":"357","DOI":"10.1145\/2676726.2677007","volume-title":"42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL \u201915). Sriram","author":"Pous Damien","year":"2015","unstructured":"Damien Pous. 2015. Symbolic Algorithms for Language Equivalence and Kleene Algebra with Tests. In 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL \u201915). Sriram K. Rajamani and David Walker (Eds.), ACM, New York, NY, 357\u2013368. DOI: 10.1145\/2676726.2677007"},{"key":"e_1_3_3_62_1","first-page":"307","volume-title":"31st Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS \u201916). Martin Grohe, Eric Koskinen, and Natarajan Shankar (","author":"Pous Damien","year":"2016","unstructured":"Damien Pous. 2016. Coinduction all the way up. In 31st Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS \u201916). Martin Grohe, Eric Koskinen, and Natarajan Shankar (Eds.), ACM, New York, NY, 307\u2013316. DOI: 10.1145\/2933575.2934564"},{"key":"e_1_3_3_63_1","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1145\/2676724.2693167","volume-title":"2015 Conference on Certified Programs and Proofs (CPP \u201915)","author":"Ramananandro Tahina","year":"2015","unstructured":"Tahina Ramananandro, Zhong Shao, Shu-Chun Weng, J\u00e9r\u00e9mie Koenig, and Yuchen Fu. 2015. A compositional semantics for verified separate compilation and linking. In 2015 Conference on Certified Programs and Proofs (CPP \u201915). Xavier Leroy and Alwen Tiu (Eds.), ACM, New York, NY, 3\u201314. DOI: 10.1145\/2676724.2693167"},{"key":"e_1_3_3_64_1","first-page":"15","volume-title":"Lecture Notes in Computer Science","volume":"3525","author":"Roscoe A. W.","year":"2004","unstructured":"A. W. Roscoe. 2004. Seeing beyond divergence. In Communicating Sequential Processes: The First 25 Years, Symposium on the Occasion of 25 Years of CSP, Revised Invited Papers. Ali E. Abdallah, Cliff B. Jones, and Jeff W. Sanders (Eds.), Lecture Notes in Computer Science, Vol. 3525, Springer, 15\u201335. DOI: 10.1007\/11423348_2"},{"key":"e_1_3_3_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84882-258-0"},{"key":"e_1_3_3_66_1","volume-title":"Outline of a Mathematical Theory of Computation","year":"1970","unstructured":"Dana Scott. 1970. Outline of a Mathematical Theory of Computation. Oxford University Computing Laboratory, Programming Research Group Oxford."},{"key":"e_1_3_3_67_1","volume-title":"Toward a Mathematical Semantics for Computer Languages","author":"Scott Dana S","year":"1971","unstructured":"Dana S Scott and Christopher Strachey. 1971. Toward a Mathematical Semantics for Computer Languages. Vol. 1. Oxford University Computing Laboratory, Programming Research Group Oxford."},{"key":"e_1_3_3_68_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90048-X"},{"key":"e_1_3_3_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371091"},{"key":"e_1_3_3_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571232"},{"key":"e_1_3_3_71_1","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1145\/2676726.2676985","volume-title":"42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL \u201915)","author":"Stewart Gordon","year":"2015","unstructured":"Gordon Stewart, Lennart Beringer, Santiago Cuellar, and Andrew W. Appel. 2015. Compositional CompCert. In 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL \u201915). Sriram K. Rajamani and David Walker(Eds.), ACM, New York, NY, 275\u2013287. DOI: 10.1145\/2676726.2676985"},{"key":"e_1_3_3_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290349"},{"key":"e_1_3_3_73_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.ENTCS.2019.09.016"},{"key":"e_1_3_3_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290375"},{"key":"e_1_3_3_75_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(85)90037-4"},{"key":"e_1_3_3_76_1","doi-asserted-by":"crossref","unstructured":"Glynn Winskel. 1993. The Formal Semantics of Programming Languages\u2014An Introduction. MIT Press.","DOI":"10.7551\/mitpress\/3054.001.0001"},{"key":"e_1_3_3_77_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24756-2_4"},{"key":"e_1_3_3_78_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371119"},{"key":"e_1_3_3_79_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473572"},{"key":"e_1_3_3_80_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632914"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3797874","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,23]],"date-time":"2026-03-23T09:03:10Z","timestamp":1774256590000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3797874"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,3,23]]},"references-count":79,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2026,3,31]]}},"alternative-id":["10.1145\/3797874"],"URL":"https:\/\/doi.org\/10.1145\/3797874","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,3,23]]},"assertion":[{"value":"2024-12-05","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-01-23","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-03-23","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}