{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,3]],"date-time":"2026-03-03T00:48:33Z","timestamp":1772498913480,"version":"3.50.1"},"reference-count":57,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2021,8,19]],"date-time":"2021-08-19T00:00:00Z","timestamp":1629331200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"ONR","award":["00014-17-1-2930"],"award-info":[{"award-number":["00014-17-1-2930"]}]},{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["1521539"],"award-info":[{"award-number":["1521539"]}],"id":[{"id":"10.13039\/100000001","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":[[2021,8,22]]},"abstract":"<jats:p>This paper presents a novel formal semantics, mechanized in Coq, for a large, sequential subset of the LLVM IR. In contrast to previous approaches, which use relationally-specified operational semantics, this new semantics is based on monadic interpretation of interaction trees, a structure that provides a more compositional approach to defining language semantics while retaining the ability to extract an executable interpreter. Our semantics handles many of the LLVM IR's non-trivial language features and is constructed modularly in terms of event handlers, including those that deal with nondeterminism in the specification. We show how this semantics admits compositional reasoning principles derived from the interaction trees equational theory of weak bisimulation, which we extend here to better deal with nondeterminism, and we use them to prove that the extracted reference interpreter faithfully refines the semantic model. We validate the correctness of the semantics by evaluating it on unit tests and LLVM IR programs generated by HELIX.<\/jats:p>","DOI":"10.1145\/3473572","type":"journal-article","created":{"date-parts":[[2021,8,19]],"date-time":"2021-08-19T10:44:29Z","timestamp":1629369869000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":30,"title":["Modular, compositional, and executable formal semantics for LLVM IR"],"prefix":"10.1145","volume":"5","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4585-6470","authenticated-orcid":false,"given":"Yannick","family":"Zakowski","sequence":"first","affiliation":[{"name":"Inria, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3469-7219","authenticated-orcid":false,"given":"Calvin","family":"Beck","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3388-1257","authenticated-orcid":false,"given":"Irene","family":"Yoon","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1617-3259","authenticated-orcid":false,"given":"Ilia","family":"Zaichuk","sequence":"additional","affiliation":[{"name":"Taras Shevchenko National University of Kyiv, Ukraine"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9145-3288","authenticated-orcid":false,"given":"Vadim","family":"Zaliva","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA \/ Digamma.ai, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3516-1512","authenticated-orcid":false,"given":"Steve","family":"Zdancewic","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, USA"}]}],"member":"320","published-online":{"date-parts":[[2021,8,19]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19718-5_1"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371075"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964003"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535876"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/3049832.3049844"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_3"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706312"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/115372.115320"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2018.2873289"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676975"},{"key":"e_1_2_2_12_1","volume-title":"Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation (OSDI\u201916)","author":"Gu Ronghui","year":"2016"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192381"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429093"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2738005"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837642"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192377"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293880.3294106"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676724.2693571"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535841"},{"key":"e_1_2_2_22_1","volume-title":"Pierce","author":"Lampropoulos Leonidas","year":"2018"},{"key":"e_1_2_2_23_1","volume-title":"LLVM: A Compilation Framework for Lifelong Program Analysis and Transformation.","author":"Lattner Chris","year":"2004"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276495"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3140587.3062343"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_2_2_27_1","unstructured":"Xavier Leroy Andrew W. Appel Sandrine Blazy and Gordon Stewart. 2012. The CompCert Memory Model Version 2. INRIA 26. https:\/\/hal.inria.fr\/hal-00703441  Xavier Leroy Andrew W. Appel Sandrine Blazy and Gordon Stewart. 2012. The CompCert Memory Model Version 2. INRIA 26. https:\/\/hal.inria.fr\/hal-00703441"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2007.12.004"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2020.7"},{"key":"e_1_2_2_30_1","volume-title":"Gunter","author":"Li Liyi","year":"2018"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454030"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2813885.2737965"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371072"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21668-3_24"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290380"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908081"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3140587.3062372"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784764"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_23"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341689"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1023064908962"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1561\/9781680835953"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2010.03.012"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2487241.2487248"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371091"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/174675.178068"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676985"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341707"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.3744225"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290375"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371119"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993532"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373813"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3264738.3264739"},{"key":"e_1_2_2_55_1","volume-title":"Reification of Shallow-Embedded DSLs in Coq with Automated Verification. In International Workshop on Coq for Programming Languages (CoqPL).","author":"Zaliva Vadim","year":"2019"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-63618-0_3"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103621.2103709"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/2499370.2462164"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3473572","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3473572","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3473572","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:28:15Z","timestamp":1750195695000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3473572"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,8,19]]},"references-count":57,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2021,8,22]]}},"alternative-id":["10.1145\/3473572"],"URL":"https:\/\/doi.org\/10.1145\/3473572","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,8,19]]},"assertion":[{"value":"2021-08-19","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}