{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:43:35Z","timestamp":1780994615476,"version":"3.54.1"},"reference-count":37,"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-sa\/4.0\/"}],"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>Systems programmers need fine-grained control over the memory layout of data structures, both to produce performant code and to comply with well-defined interfaces imposed by existing code, standardised protocols or hardware. Code that manipulates these low-level representations in memory is hard to get right. Traditionally, this problem is addressed by the implementation of tedious marshalling code to convert between compiler-selected data representations and the desired compact data formats. Such marshalling code is error-prone and can lead to a significant runtime overhead due to excessive copying. While there are many languages and systems that address the correctness issue, by automating the generation and, in some cases, the verification of the marshalling code, the performance overhead introduced by the marshalling code remains. In particular for systems code, this overhead can be prohibitive. In this work, we address both the correctness and the performance problems.<\/jats:p>\n          <jats:p>We present a data layout description language and data refinement framework, called Dargent, which allows programmers to declaratively specify how algebraic data types are laid out in memory. Our solution is applied to the Cogent language, but the general ideas behind our solution are applicable to other settings. The Dargent framework generates C code that manipulates data directly with the desired memory layout, while retaining the formal proof that this generated C code is correct with respect to the functional semantics. This added expressivity removes the need for implementing and verifying marshalling code, which eliminates copying, smoothens interoperability with surrounding systems, and increases the trustworthiness of the overall system.<\/jats:p>","DOI":"10.1145\/3571240","type":"journal-article","created":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T21:58:14Z","timestamp":1673474294000},"page":"1369-1395","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Dargent: A Silver Bullet for Verified Data Layout Refinement"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0854-2464","authenticated-orcid":false,"given":"Zilin","family":"Chen","sequence":"first","affiliation":[{"name":"UNSW, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9299-641X","authenticated-orcid":false,"given":"Ambroise","family":"Lafont","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2765-4269","authenticated-orcid":false,"given":"Liam","family":"O'Connor","sequence":"additional","affiliation":[{"name":"University of Edinburgh, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1442-5387","authenticated-orcid":false,"given":"Gabriele","family":"Keller","sequence":"additional","affiliation":[{"name":"Utrecht University, Netherlands"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1323-8566","authenticated-orcid":false,"given":"Craig","family":"McLaughlin","sequence":"additional","affiliation":[{"name":"UNSW, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8737-4202","authenticated-orcid":false,"given":"Vincent","family":"Jackson","sequence":"additional","affiliation":[{"name":"University of Melbourne, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4785-2836","authenticated-orcid":false,"given":"Christine","family":"Rizkallah","sequence":"additional","affiliation":[{"name":"University of Melbourne, Australia"}],"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.1145\/2872362.2872404"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45821-2_4"},{"key":"e_1_2_1_3_1","volume-title":"Nail: A Practical Tool for Parsing and Generating Data Formats. In 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI 14)","author":"Bangert Julian","year":"2014","unstructured":"Julian Bangert and Nickolai Zeldovich . 2014 . Nail: A Practical Tool for Parsing and Generating Data Formats. In 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI 14) . USENIX Association, Broomfield, CO. 615\u2013628. isbn:978-1-93 1971-16-4 https:\/\/www.usenix.org\/conference\/osdi14\/technical-sessions\/presentation\/bangert Julian Bangert and Nickolai Zeldovich. 2014. Nail: A Practical Tool for Parsing and Generating Data Formats. In 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI 14). USENIX Association, Broomfield, CO. 615\u2013628. isbn:978-1-931971-16-4 https:\/\/www.usenix.org\/conference\/osdi14\/technical-sessions\/presentation\/bangert"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57529-4_42"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7220452"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3567512.3567520"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3497775.3503686"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3357765.3359519"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341686"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159842.1159851"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1086365.1086387"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065046"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1938551.1938556"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133850.3133861"},{"key":"#cr-split#-e_1_2_1_15_1.1","unstructured":"Juliana Franco Alexandros Tasos Sophia Drossopoulou Tobias Wrigstad and Susan Eisenbach. 2019. Safely Abstracting Memory Layouts. https:\/\/doi.org\/10.48550\/ARXIV.1901.08006 10.48550\/ARXIV.1901.08006"},{"key":"#cr-split#-e_1_2_1_15_1.2","unstructured":"Juliana Franco Alexandros Tasos Sophia Drossopoulou Tobias Wrigstad and Susan Eisenbach. 2019. Safely Abstracting Memory Layouts. https:\/\/doi.org\/10.48550\/ARXIV.1901.08006"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594296"},{"key":"e_1_2_1_17_1","unstructured":"Steve Klabnik and Carol Nichols. 2022. The Rust Programming Language. https:\/\/doc.rust-lang.org\/book\/ch04-02-references-and-borrowing.html \t\t\t\t  Steve Klabnik and Carol Nichols. 2022. The Rust Programming Language. https:\/\/doc.rust-lang.org\/book\/ch04-02-references-and-borrowing.html"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190231"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/347059.347563"},{"key":"e_1_2_1_20_1","volume-title":"Recursive Types for Cogent","author":"Murray Emmet","unstructured":"Emmet Murray . 2019. Recursive Types for Cogent . UNSW . Sydney, Australia . https:\/\/github.com\/emmet-m\/thesis Emmet Murray. 2019. Recursive Types for Cogent. UNSW. Sydney, Australia. https:\/\/github.com\/emmet-m\/thesis"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.26190\/unsworks\/21495"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951940"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679682100023X"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03418-4_9"},{"key":"e_1_2_1_26_1","volume-title":"Refinement Types for Cogent","author":"Paradeza Blaise","unstructured":"Blaise Paradeza . 2020. Refinement Types for Cogent . UNSW . Sydney, Australia . https:\/\/people.eng.unimelb.edu.au\/rizkallahc\/theses\/blaise-paradeza-honours-thesis.pdf Blaise Paradeza. 2020. Refinement Types for Cogent. UNSW. Sydney, Australia. https:\/\/people.eng.unimelb.edu.au\/rizkallahc\/theses\/blaise-paradeza-honours-thesis.pdf"},{"key":"e_1_2_1_27_1","volume-title":"EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats. In 28th USENIX Security Symposium (USENIX Security 19)","author":"Ramananandro Tahina","year":"2019","unstructured":"Tahina Ramananandro , Antoine Delignat-Lavaud , Cedric Fournet , Nikhil Swamy , Tej Chajed , Nadim Kobeissi , and Jonathan Protzenko . 2019 . EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats. In 28th USENIX Security Symposium (USENIX Security 19) . USENIX Association, Santa Clara, CA. 1465\u20131482. isbn:978-1-939133-06-9 https:\/\/www.usenix.org\/conference\/usenixsecurity19\/presentation\/delignat-lavaud Tahina Ramananandro, Antoine Delignat-Lavaud, Cedric Fournet, Nikhil Swamy, Tej Chajed, Nadim Kobeissi, and Jonathan Protzenko. 2019. EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats. In 28th USENIX Security Symposium (USENIX Security 19). USENIX Association, Santa Clara, CA. 1465\u20131482. isbn:978-1-939133-06-9 https:\/\/www.usenix.org\/conference\/usenixsecurity19\/presentation\/delignat-lavaud"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-43144-4_20"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32275-7_26"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2021.30"},{"key":"e_1_2_1_31_1","unstructured":"The seL4 developers. 2022. The seL4 Microkernel. https:\/\/sel4.systems\/ \t\t\t\t  The seL4 developers. 2022. The seL4 Microkernel. https:\/\/sel4.systems\/"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3122975.3122979"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314631"},{"key":"e_1_2_1_34_1","unstructured":"Philip Wadler. 1990. Linear Types Can Change the World!. In Programming Concepts and Methods. North-Holland 561. \t\t\t\t  Philip Wadler. 1990. Linear Types Can Change the World!. In Programming Concepts and Methods. North-Holland 561."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1929501.1929511"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293880.3294105"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571240","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3571240","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:08:22Z","timestamp":1750183702000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571240"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,9]]},"references-count":37,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2023,1,9]]}},"alternative-id":["10.1145\/3571240"],"URL":"https:\/\/doi.org\/10.1145\/3571240","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"}}]}}