{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:44:29Z","timestamp":1780994669296,"version":"3.54.1"},"reference-count":56,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2023,1,9]],"date-time":"2023-01-09T00:00:00Z","timestamp":1673222400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"Dutch Research Council","award":["016.Veni.192.259"],"award-info":[{"award-number":["016.Veni.192.259"]}]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["101003349"],"award-info":[{"award-number":["101003349"]}],"id":[{"id":"10.13039\/501100000781","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":[[2023,1,9]]},"abstract":"<jats:p>Prior work on multi-language program verification has achieved impressive results, including the compositional verification of complex compilers. But the existing approaches to this problem impose a variety of restrictions on the overall structure of multi-language programs (e.g. fixing the source language, fixing the set of involved languages, fixing the memory model, or fixing the semantics of interoperation). In this paper, we explore the problem of how to avoid such global restrictions.<\/jats:p>\n          <jats:p>\n            Concretely, we present\n            <jats:bold>DimSum<\/jats:bold>\n            : a new,\n            <jats:italic>decentralized<\/jats:italic>\n            approach to multi-language semantics and verification, which we have implemented in the Coq proof assistant. Decentralization means that we can define and reason about languages independently from each other (as independent\n            <jats:italic>modules<\/jats:italic>\n            communicating via events), but also combine and translate between them when necessary (via a library of combinators).\n          <\/jats:p>\n          <jats:p>We apply DimSum to a high-level imperative language Rec (with an abstract memory model and function calls), a low-level assembly language Asm (with a concrete memory model, arbitrary jumps, and syscalls), and a mathematical specification language Spec. We evaluate DimSum on two case studies: an Asm library extending Rec with support for pointer comparison, and a coroutine library for Rec written in Asm. In both cases, we show how DimSum allows the Asm libraries to be abstracted to Rec-level specifications, despite the behavior of the Asm libraries not being syntactically expressible in Rec itself. We also verify an optimizing multi-pass compiler from Rec to Asm, showing that it is compatible with these Asm libraries.<\/jats:p>","DOI":"10.1145\/3571220","type":"journal-article","created":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T21:58:14Z","timestamp":1673474294000},"page":"775-805","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":17,"title":["DimSum: A Decentralized Approach to Multi-language Semantics and Verification"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4591-743X","authenticated-orcid":false,"given":"Michael","family":"Sammler","sequence":"first","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5424-9002","authenticated-orcid":false,"given":"Simon","family":"Spies","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7093-3824","authenticated-orcid":false,"given":"Youngju","family":"Song","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9179-5827","authenticated-orcid":false,"given":"Emanuele","family":"D'Osualdo","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}],"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, Netherlands"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0888-3093","authenticated-orcid":false,"given":"Deepak","family":"Garg","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}],"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, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2023,1,11]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2010.30"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034830"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0055622"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596567"},{"key":"e_1_2_1_5_1","unstructured":"Nick Benton and Chung-Kil Hur. 2010. Realizability and compositional compiler correctness for a polymorphic language. Microsoft Research. https:\/\/sf.snu.ac.kr\/publications\/cccmsrtr.pdf \t\t\t\t  Nick Benton and Chung-Kil Hur. 2010. Realizability and compositional compiler correctness for a polymorphic language. Microsoft Research. https:\/\/sf.snu.ac.kr\/publications\/cccmsrtr.pdf"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_7"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/322234.322243"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/321420.321422"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.01.016"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498689"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676975"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192381"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/359576.359585"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926402"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103666"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31987-0_29"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837642"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454097"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236772"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_26"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73420-8_58"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111042"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9099-0"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3354166.3354181"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190220"},{"key":"e_1_2_1_29_1","volume-title":"Communicating and Mobile Systems: the \u03c0 -Calculus","author":"Milner Robin","unstructured":"Robin Milner . 1999. Communicating and Mobile Systems: the \u03c0 -Calculus . Cambridge University Press . isbn:978-0-521-65869-0 Robin Milner. 1999. Communicating and Mobile Systems: the \u03c0 -Calculus. Cambridge University Press. isbn:978-0-521-65869-0"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90008-4"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784764"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236768"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.45.6"},{"key":"e_1_2_1_34_1","volume-title":"Syntax Highlighting Beyond Code Snippets. CoRR, abs\/2001.11334","author":"Patrignani Marco","year":"2020","unstructured":"Marco Patrignani . 2020. Why Should Anyone use Colours? or , Syntax Highlighting Beyond Code Snippets. CoRR, abs\/2001.11334 ( 2020 ), arxiv:2001.11334 Marco Patrignani. 2020. Why Should Anyone use Colours? or, Syntax Highlighting Beyond Code Snippets. CoRR, abs\/2001.11334 (2020), arxiv:2001.11334"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2699503"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341689"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523703"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062347"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_8"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51054-1_7"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676724.2693167"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24615-2_12"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84882-258-0"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523434"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7306313"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7306313"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371091"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571232"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428220"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676985"},{"key":"e_1_2_1_51_1","volume-title":"Tanenbaum and Herbert Bos","author":"Andrew","year":"2014","unstructured":"Andrew S. Tanenbaum and Herbert Bos . 2014 . Modern Operating Systems (4th ed.). Prentice Hall Press , USA. isbn:013359162X https:\/\/dl.acm.org\/doi\/book\/10.5555\/2655363 Andrew S. Tanenbaum and Herbert Bos. 2014. Modern Operating Systems (4th ed.). Prentice Hall Press, USA. isbn:013359162X https:\/\/dl.acm.org\/doi\/book\/10.5555\/2655363"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498703"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0015261"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660201"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290375"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371119"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571220","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3571220","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:08:21Z","timestamp":1750183701000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571220"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,9]]},"references-count":56,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2023,1,9]]}},"alternative-id":["10.1145\/3571220"],"URL":"https:\/\/doi.org\/10.1145\/3571220","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,1,9]]},"assertion":[{"value":"2023-01-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}