{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,21]],"date-time":"2026-07-21T23:04:08Z","timestamp":1784675048592,"version":"3.55.0"},"reference-count":21,"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\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["2313433, 2019285"],"award-info":[{"award-number":["2313433, 2019285"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["62372290, 62002217"],"award-info":[{"award-number":["62372290, 62002217"]}],"id":[{"id":"10.13039\/501100001809","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":[[2025,1,7]]},"abstract":"<jats:p>\n                    Formal verification is a gold standard for building reliable computer systems.\n                    <jats:italic toggle=\"yes\">Certified<\/jats:italic>\n                    systems in particular come with a formal specification, and a proof of correctness which can easily be checked by a third party.\n                  <\/jats:p>\n                  <jats:p>Unfortunately, verifying large-scale, heterogeneous systems remains out of reach of current techniques. Addressing this challenge will require the use of compositional methods capable of accommodating and interfacing a range of program verification and certified compilation techniques. In principle, compositional semantics could play a role in enabling this kind of flexibility, but in practice existing tools tend to rely on simple and specialized operational models which are difficult to interface with one another.<\/jats:p>\n                  <jats:p>To tackle this issue, we present a compositional semantics framework which can accommodate a broad range of verification techniques. Its core is a three-dimensional algebra of refinement which operates across program modules, levels of abstraction, and components of the system\u2019s state. Our framework is mechanized in the Coq proof assistant and we showcase its capabilities with multiple use cases.<\/jats:p>","DOI":"10.1145\/3704900","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"1903-1933","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Unifying Compositional Verification and Certified Compilation with a Three-Dimensional Refinement Algebra"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0009-1160-9851","authenticated-orcid":false,"given":"Yu","family":"Zhang","sequence":"first","affiliation":[{"name":"Yale University, New Haven, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3168-5925","authenticated-orcid":false,"given":"J\u00e9r\u00e9mie","family":"Koenig","sequence":"additional","affiliation":[{"name":"Yale University, New Haven, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8184-7649","authenticated-orcid":false,"given":"Zhong","family":"Shao","sequence":"additional","affiliation":[{"name":"Yale University, New Haven, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3990-2418","authenticated-orcid":false,"given":"Yuting","family":"Wang","sequence":"additional","affiliation":[{"name":"Shanghai Jiao Tong University, Shanghai, China"}],"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-19718-5_1"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-1674-2"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328487"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","unstructured":"Cristiano Calcagno Peter W. O\u2019Hearn and Hongseok Yang. 2007. Local Action and Abstract Separation Logic. In 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007). 366\u2013378. https:\/\/doi.org\/10.1109\/LICS.2007.30 10.1109\/LICS.2007.30","DOI":"10.1109\/LICS.2007.30"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656446"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676975"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192381"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622823"},{"key":"e_1_3_2_10_1","unstructured":"J\u00e9r\u00e9mie Koenig. 2016\u20132024. Coqrel: a binary logical relations library for the Coq proof assistant. https:\/\/github.com\/CertiKOS\/coqrel"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394799"},{"key":"e_1_3_2_12_1","doi-asserted-by":"crossref","unstructured":"J\u00e9r\u00e9mie Koenig and Zhong Shao. 2021. CompCertO: compiling certified open C components. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. 1095\u20131109.","DOI":"10.1145\/3453483.3454097"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293880.3294106"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190215.1190220"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498703"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571220"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371091"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571232"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632914"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","unstructured":"Yu Zhang J\u00e9r\u00e9mie Koenig Yuting Wang and Zhong Shao. 2024a. Unifying compositional verification and certified compilation with a three-dimensional refinement algebra (artifact). https:\/\/doi.org\/10.5281\/zenodo.14202535 10.5281\/zenodo.14202535","DOI":"10.5281\/zenodo.14202535"},{"key":"e_1_3_2_22_1","volume-title":"Unifying compositional verification and certified compilation with a three-dimensional refinement algebra (extended version)","author":"Zhang Yu","year":"2024","unstructured":"Yu Zhang, J\u00e9r\u00e9mie Koenig, Yuting Wang, and Zhong Shao. 2024b. Unifying compositional verification and certified compilation with a three-dimensional refinement algebra (extended version). Technical Report YALEU\/DCS\/TR1572. Yale University."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704900","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704900","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:17:30Z","timestamp":1770200250000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704900"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":21,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704900"],"URL":"https:\/\/doi.org\/10.1145\/3704900","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-11","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"}}]}}