{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T21:01:09Z","timestamp":1751662869716,"version":"3.41.0"},"reference-count":42,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2019,10,10]],"date-time":"2019-10-10T00:00:00Z","timestamp":1570665600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1521523, 1715154, 1763399"],"award-info":[{"award-number":["1521523, 1715154, 1763399"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["FA8750-15-C-0082"],"award-info":[{"award-number":["FA8750-15-C-0082"]}],"id":[{"id":"10.13039\/100000185","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":[[2019,10,10]]},"abstract":"<jats:p>Writing certifiably correct system software is still very labor-intensive, and current programming languages are not well suited for the task. Proof assistants work best on programs written in a high-level functional style, while operating systems need low-level control over the hardware. We present DeepSEA, a language which provides support for layered specification and abstraction refinement, effect encapsulation and composition, and full equational reasoning. A single DeepSEA program is automatically compiled into a certified ``layer'' consisting of a C program (which is then compiled into assembly by CompCert), a low-level functional Coq specification, and a formal (Coq) proof that the C program satisfies the specification. Multiple layers can be composed and interleaved with manual proofs to ascribe a high-level specification to a program by stepwise refinement. We evaluate the language by using it to reimplement two existing verified programs: a SHA-256 hash function and an OS kernel page table manager. This new style of programming language design can directly support the development of correct-by-construction system software.<\/jats:p>","DOI":"10.1145\/3360562","type":"journal-article","created":{"date-parts":[[2019,10,11]],"date-time":"2019-10-11T14:53:33Z","timestamp":1570805613000},"page":"1-27","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["DeepSEA: a language for certified system software"],"prefix":"10.1145","volume":"3","author":[{"given":"Vilhelm","family":"Sj\u00f6berg","sequence":"first","affiliation":[{"name":"Yale University, USA \/ CertiK, USA"}]},{"given":"Yuyang","family":"Sang","sequence":"additional","affiliation":[{"name":"Yale University, USA"}]},{"given":"Shu-chun","family":"Weng","sequence":"additional","affiliation":[{"name":"Yale University, USA"}]},{"given":"Zhong","family":"Shao","sequence":"additional","affiliation":[{"name":"Yale University, USA"}]}],"member":"320","published-online":{"date-parts":[[2019,10,10]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2872362.2872404"},{"volume-title":"Matthieu Sozeau, and Matthew Weaver.","year":"2017","author":"Anand Abhishek","key":"e_1_2_2_2_1"},{"key":"e_1_2_2_3_1","volume-title":"Verified Software Toolchain. In ESOP\u201911: European Symposium on Programming, Gilles Barthe (Ed.). LNCS","volume":"6602","author":"Appel Andrew","year":"2011"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2701415"},{"key":"e_1_2_2_5_1","unstructured":"Apple. 2013\u20132015. The Swift Programming Language. http:\/\/developer.apple.com\/swift .  Apple. 2013\u20132015. The Swift Programming Language. http:\/\/developer.apple.com\/swift ."},{"volume-title":"Safety and Performance in the SPIN Operating System. In 15th ACM Symposium on Operating System Principles. 267\u2013284","author":"Brian","key":"e_1_2_2_6_1"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-19458-5_2"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-77935-5_3"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9148-3"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993526"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908100"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677006"},{"key":"e_1_2_2_13_1","unstructured":"Olivier Gay. 2005. Software implementation in C of the FIPS 198 Keyed-Hash Message Authentication Code HMAC for SHA2. https:\/\/github.com\/ogay\/hmac  Olivier Gay. 2005. Software implementation in C of the FIPS 198 Keyed-Hash Message Authentication Code HMAC for SHA2. https:\/\/github.com\/ogay\/hmac"},{"volume-title":"The Java Language Specification","author":"Gosling James","key":"e_1_2_2_14_1"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32347-8_8"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594296"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512563"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676975"},{"volume-title":"Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation (OSDI\u201916)","year":"2016","author":"Gu Ronghui","key":"e_1_2_2_19_1"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192381"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_22"},{"volume-title":"Computer Systems Reliability, State of the Art Report","author":"Hoare Tony","key":"e_1_2_2_22_1"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1243418.1243424"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-014-0326-7"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2560537"},{"key":"e_1_2_2_26_1","first-page":"2","article-title":"Software Synthesis","volume":"55","author":"Kuncak Viktor","year":"2012","journal-title":"Procedures. Commun. ACM"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48959-2_17"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/800055.802036"},{"volume-title":"CRiSIS 2016 - 11th International Conference on Risks and Security of Internet and Systems.","author":"Mangano Fr\u00e9d\u00e9ric","key":"e_1_2_2_30_1"},{"key":"e_1_2_2_31_1","first-page":"3","article-title":"Automatic Program","volume":"14","author":"Manna Zohar","year":"1971","journal-title":"Synthesis. Commun. ACM"},{"volume-title":"Drafts of the ECMA TC39\/TG3 standardization process","year":"2001","author":"Microsoft Corp.","key":"e_1_2_2_32_1"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1989.39155"},{"volume-title":"Systems Programming with Modula-3","author":"Nelson Greg","key":"e_1_2_2_35_1"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951940"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110261"},{"volume-title":"Proc. 37th ACM Symposium on Principles of Programming Languages. 313\u2013326","author":"Srivastava Saurabh","key":"e_1_2_2_41_1"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951924"},{"key":"e_1_2_2_43_1","unstructured":"The Coq development team. 1999 \u2013 2014. The Coq proof assistant. http:\/\/coq.inria.fr .  The Coq development team. 1999 \u2013 2014. The Coq proof assistant. http:\/\/coq.inria.fr ."},{"key":"e_1_2_2_44_1","unstructured":"The Kestrel Institute. 2015. The SpecWare System. www.kestrel.edu\/home\/prototypes\/specware.html .  The Kestrel Institute. 2015. The SpecWare System. www.kestrel.edu\/home\/prototypes\/specware.html ."},{"key":"e_1_2_2_45_1","unstructured":"The Rust Team. 2011\u20132015. The Rust Programming Language. http:\/\/www.rust- lang.org .  The Rust Team. 2011\u20132015. The Rust Programming Language. http:\/\/www.rust- lang.org ."},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2666356.2594340"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360562","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3360562","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3360562","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:22:59Z","timestamp":1750202579000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360562"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10,10]]},"references-count":42,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2019,10,10]]}},"alternative-id":["10.1145\/3360562"],"URL":"https:\/\/doi.org\/10.1145\/3360562","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2019,10,10]]},"assertion":[{"value":"2019-10-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}