{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T10:08:20Z","timestamp":1781258900716,"version":"3.54.1"},"reference-count":111,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2021,10,27]],"date-time":"2021-10-27T00:00:00Z","timestamp":1635292800000},"content-version":"unspecified","delay-in-days":299,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>This paper presents a framework aimed at significantly reducing the cost of proving functional correctness for low-level operating systems components. The framework is designed around a new functional programming language, Cogent. A central aspect of the language is its uniqueness type system, which eliminates the need for a trusted runtime or garbage collector while still guaranteeing memory safety, a crucial property for safety and security. Moreover, it allows us to assign two semantics to the language: The first semantics is imperative, suitable for efficient C code generation, and the second is purely functional, providing a user-friendly interface for equational reasoning and verification of higher-level correctness properties. The refinement theorem connecting the two semantics allows the compiler to produce a proof via translation validation certifying the correctness of the generated C code with respect to the semantics of the Cogent source program. We have demonstrated the effectiveness of our framework for implementation and for verification through two file system implementations.<\/jats:p>","DOI":"10.1017\/s095679682100023x","type":"journal-article","created":{"date-parts":[[2021,10,27]],"date-time":"2021-10-27T00:42:57Z","timestamp":1635295377000},"update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":17,"title":["Cogent: uniqueness types and certifying compilation"],"prefix":"10.1017","volume":"31","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2765-4269","authenticated-orcid":false,"given":"LIAM","family":"O\u2019CONNOR","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"ZILIN","family":"CHEN","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"CHRISTINE","family":"RIZKALLAH","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"VINCENT","family":"JACKSON","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"SIDNEY","family":"AMANI","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"GERWIN","family":"KLEIN","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"TOBY","family":"MURRAY","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"THOMAS","family":"SEWELL","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"GABRIELE","family":"KELLER","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2021,10,27]]},"reference":[{"key":"S095679682100023X_ref16","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796820000283"},{"key":"S095679682100023X_ref54","doi-asserted-by":"crossref","unstructured":"Hofmann, M. (2000) A type system for bounded space and functional in-place update. In European Symposium on Programming. Lecture Notes in Computer Science, vol. 1782, pp. 165\u2013179.","DOI":"10.1007\/3-540-46425-5_11"},{"key":"S095679682100023X_ref43","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32347-8_8"},{"key":"S095679682100023X_ref25","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351266"},{"key":"S095679682100023X_ref35","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85373-2_12"},{"key":"S095679682100023X_ref39","doi-asserted-by":"crossref","unstructured":"Ernst, G. , Schellhorn, G. , Haneberg, D. , Pf\u00e4hler, J. and Reif, W. (2013) Verification of a virtual filesystem switch. In Verified Software: Theories, Tools and Experiments. Lecture Notes in Computer Science, vol. 8164. Springer, pp. 242\u2013261.","DOI":"10.1007\/978-3-642-54108-7_13"},{"key":"S095679682100023X_ref1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-013-9289-2"},{"key":"S095679682100023X_ref58","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"S095679682100023X_ref55","unstructured":"Jim, T. , Morrisett, J. G. , Grossman, D. , Hicks, M. W. , Cheney, J. and Wang, Y. (2002) Cyclone: A safe dialect of c. In USENIX Annual Technical Conference. USENIX, pp. 275\u2013288."},{"key":"S095679682100023X_ref30","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-88194-0_5"},{"key":"S095679682100023X_ref67","doi-asserted-by":"publisher","DOI":"10.1016\/j.cosrev.2010.09.009"},{"key":"S095679682100023X_ref49","first-page":"130","volume-title":"Principles of Programming Languages","author":"Harper","year":"1995"},{"key":"S095679682100023X_ref68","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863584"},{"key":"S095679682100023X_ref97","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-05089-3_13"},{"key":"S095679682100023X_ref101","unstructured":"Sison, R. and Murray, T. (2019) Verifying that a compiler preserves concurrent value-dependent information-flow security. In 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9\u201312, 2019, Portland, OR , USA, Harrison, J. , O\u2019Leary, J. & Tolmach, A. (eds). LIPIcs 141. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, pp. 27:1\u201327:19."},{"key":"S095679682100023X_ref7","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.196.1"},{"key":"S095679682100023X_ref24","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784741"},{"key":"S095679682100023X_ref33","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378811"},{"key":"S095679682100023X_ref59","first-page":"179","volume-title":"Principles of Programming Languages","author":"Kumar","year":"2014"},{"key":"S095679682100023X_ref21","unstructured":"Chen, Z. , Di Meglio, M. , O\u2019Connor, L. , Susarla Ajay, P. , Rizkallah, C. and Keller, G. (2019) A Data Layout Description Language for Cogent (extended abstract). http:\/\/ssrg.nicta.com\/publications\/csiro_full_text\/Chen_DOSRK_19.pdf. At Principles of Secure Compilation (PriSC)."},{"key":"S095679682100023X_ref86","first-page":"13","article-title":"Structured specifications and interactive proofs with KIV. In Automated Deduction \u2013 A Basis for Applications. Applied Logic","volume":"9","author":"Reif","year":"1998","journal-title":"Series"},{"key":"S095679682100023X_ref44","doi-asserted-by":"publisher","DOI":"10.1145\/2666356.2594296"},{"key":"S095679682100023X_ref22","doi-asserted-by":"publisher","DOI":"10.1145\/3144555.3144556"},{"key":"S095679682100023X_ref53","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.12.018"},{"key":"S095679682100023X_ref51","unstructured":"Hawblitzel, C. , Howell, J. , Lorch, J. R. , Narayan, A. , Parno, B. , Zhang, D. and Zill, B. (2014) Ironclad apps: End-to-end security via automated full-system verification. In Operating Systems Design and Implementation, pp. 165\u2013181."},{"key":"S095679682100023X_ref56","doi-asserted-by":"crossref","unstructured":"Keller, G. , Murray, T. , Amani, S. , O\u2019Connor, L. , Chen, Z. , Ryzhyk, L. , Klein, G. and Heiser, G. (2013) File systems deserve verification too! In Programming Languages and Operating Systems, pp. 1\u20137.","DOI":"10.1145\/2525528.2525530"},{"key":"S095679682100023X_ref62","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"S095679682100023X_ref79","unstructured":"OpenSSL. (2014) Apple\u2019s SSL\/TLS bug. Accessed March 2015. Available at: https:\/\/www.imperialviolet.org\/2014\/02\/22\/applebug.html."},{"key":"S095679682100023X_ref70","unstructured":"Murray, E. (2019) Recursive Types For Cogent. Honours thesis, UNSW Sydney, Computer Science & Engineering."},{"key":"S095679682100023X_ref13","unstructured":"Bevier, W. , Cohen, R. and Turner, J. (1995) A Specification for the Synergy File System. Tech. rept. Technical Report 120. Computational Logic Inc., Austin, Texas, USA."},{"key":"S095679682100023X_ref76","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951940"},{"key":"S095679682100023X_ref40","doi-asserted-by":"publisher","DOI":"10.1145\/113445.113468"},{"key":"S095679682100023X_ref28","doi-asserted-by":"crossref","unstructured":"Coquand, T. and Paulin, C. (1988) Inductively defined types. In International Conference on Computer Logic, pp. 50\u201366.","DOI":"10.1007\/3-540-52335-9_47"},{"key":"S095679682100023X_ref48","unstructured":"Gunawi, H. S. , Rajimwale, A. , Arpaci-Dusseau, A. C. and Arpaci-Dusseau, R. H. (2008) SQCK: A declarative file system checker. In Operating Systems Design and Implementation. USENIX Association, pp. 131\u2013146."},{"key":"S095679682100023X_ref52","unstructured":"Heartbleed. (2014) The Heartbleed Bug. http:\/\/heartbleed.com, Accessed March 2015. Available at: https:\/\/www.openssl.org\/news\/secadv_20140407.txt."},{"key":"S095679682100023X_ref87","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-06859-7_148"},{"key":"S095679682100023X_ref6","doi-asserted-by":"publisher","DOI":"10.1145\/2954680.2872404"},{"key":"S095679682100023X_ref82","doi-asserted-by":"publisher","DOI":"10.1145\/1950365.1950401"},{"key":"S095679682100023X_ref31","unstructured":"Dang, V. (2020) Flogent: An Information Flow Security Feature for Cogent. Honours thesis, UNSW Sydney, Computer Science & Engineering."},{"key":"S095679682100023X_ref46","first-page":"595","volume-title":"Principles of Programming Languages","author":"Gu","year":"2015"},{"key":"S095679682100023X_ref45","doi-asserted-by":"publisher","DOI":"10.1145\/2103799.2103803"},{"key":"S095679682100023X_ref72","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9"},{"key":"S095679682100023X_ref75","unstructured":"O\u2019Connor, L. (2019) Type Systems for Systems Types. PhD thesis, University of New South Wales."},{"key":"S095679682100023X_ref78","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-55253-7_23"},{"key":"S095679682100023X_ref98","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32275-7_26"},{"key":"S095679682100023X_ref34","volume-title":"Cambridge Tracts in Theoretical Computer Science","volume":"46","author":"de Roever","year":"1998"},{"key":"S095679682100023X_ref12","volume-title":"Principles of Programming Languages","author":"Bernardy","year":"2017"},{"key":"S095679682100023X_ref80","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268134"},{"key":"S095679682100023X_ref37","volume-title":"A Discipline of Programming","author":"Dijkstra","year":"1997"},{"key":"S095679682100023X_ref89","unstructured":"Rizkallah, C. (2015) Verification of Program Computations. PhD thesis, Saarland University."},{"key":"S095679682100023X_ref95","first-page":"41","author":"Saha","year":"2011"},{"key":"S095679682100023X_ref14","doi-asserted-by":"publisher","DOI":"10.1145\/200836.200880"},{"key":"S095679682100023X_ref64","unstructured":"Lollipop. (2014) Memory Leak in Android Lollipop\u2019s rendering engine. Accessed March 2015. Available at: https:\/\/code.google.com\/p\/android\/issues\/detail?id=79729#c177."},{"key":"S095679682100023X_ref96","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43652-3_2"},{"key":"S095679682100023X_ref104","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.13"},{"key":"S095679682100023X_ref81","first-page":"305","volume-title":"Architectural Support for Programming Languages and Operating Systems","author":"Palix","year":"2011"},{"key":"S095679682100023X_ref99","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462183"},{"key":"S095679682100023X_ref2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9123-z"},{"key":"S095679682100023X_ref19","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034828"},{"key":"S095679682100023X_ref61","unstructured":"Leinenbach, D. (2010) Compiler Verification in the Context of Pervasive System Verification. PhD thesis, Saarland University."},{"key":"S095679682100023X_ref69","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1984.5010215"},{"key":"S095679682100023X_ref106","doi-asserted-by":"publisher","DOI":"10.1145\/2666356.2594340"},{"key":"S095679682100023X_ref90","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-43144-4_20"},{"key":"S095679682100023X_ref3","doi-asserted-by":"crossref","unstructured":"Alkassar, E. , Paul, W. , Starostin, A. and Tsyban, A. (2010) Pervasive verification of an OS microkernel: Inline assembly, memory consumption, concurrent devices. In Verified Software: Theories, Tools and Experiments. Lecture Notes in Computer Science, vol. 6217. Springer, pp. 71\u201385.","DOI":"10.1007\/978-3-642-15057-9_5"},{"key":"S095679682100023X_ref110","unstructured":"Yang, J. , Sar, C. and Engler, D. (2006) EXPLODE: A lightweight, general system for finding serious storage system errors. In Operating Systems Design and Implementation, pp. 131\u2013146."},{"key":"S095679682100023X_ref11","unstructured":"Beringer, L. , Petcher, A. , Ye, K. Q. and Appel, A. W. (2015) Verified correctness and security of OpenSSL HMAC. In Security Symposium. USENIX, pp. 207\u2013221."},{"key":"S095679682100023X_ref47","unstructured":"Gu, R. , Shao, Z. , Chen, H. , Wu, X. N. , Kim, J. , Sj\u00f6berg, V. and Costanzo, D. (2016) CertiKOS: An extensible architecture for building certified concurrent OS kernels. In Operating Systems Design and Implementation. ACM."},{"key":"S095679682100023X_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57529-4_42"},{"key":"S095679682100023X_ref74","unstructured":"ntfs3g. POSIX Filesystem Test Project. Accessed January, 2016. Available at: http:\/\/sourceforge.net\/p\/ntfs-3g\/pjd-fstest\/ci\/master\/tree\/."},{"key":"S095679682100023X_ref20","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815402"},{"key":"S095679682100023X_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30482-1_32"},{"key":"S095679682100023X_ref17","doi-asserted-by":"publisher","DOI":"10.1109\/12.641931"},{"key":"S095679682100023X_ref88","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11970-5_13"},{"key":"S095679682100023X_ref29","doi-asserted-by":"publisher","DOI":"10.1145\/1291151.1291199"},{"key":"S095679682100023X_ref92","unstructured":"Rust. (2014) The Rust Language. Accessed October 5, 2014. Available at: http:\/\/rust-lang.org."},{"key":"S095679682100023X_ref105","first-page":"188","volume-title":"Principles of Programming Languages","author":"Tofte","year":"1994"},{"key":"S095679682100023X_ref91","doi-asserted-by":"publisher","DOI":"10.1145\/2001420.2001434"},{"key":"S095679682100023X_ref102","doi-asserted-by":"publisher","DOI":"10.1145\/3167092"},{"key":"S095679682100023X_ref66","unstructured":"Marlow, S. (2010) Haskell 2010 Language Report."},{"key":"S095679682100023X_ref32","first-page":"79","author":"de Amorim","year":"2018"},{"key":"S095679682100023X_ref60","unstructured":"Lammich, P. (2019) Generating verified LLVM from Isabelle\/HOL. In International Conference on Interactive Theorem Proving. LIPIcs, vol. 141. Schloss Dagstuhl, pp. 22:1\u201322:19."},{"key":"S095679682100023X_ref50","unstructured":"HASP project. (2010) The Habit Programming Language: The Revised Preliminary Report. Tech. rept. http:\/\/hasp.cs.pdx.edu\/habit-report-Nov2010.pdf. Department of Computer Science, Portland State University, Portland, OR, USA."},{"key":"S095679682100023X_ref26","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_16"},{"key":"S095679682100023X_ref18","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863590"},{"key":"S095679682100023X_ref27","unstructured":"Cogent. Cogent source code and Isabelle\/HOL formalisation. Accessed March 11, 2021. Available at :https:\/\/github.com\/NICTA\/cogent."},{"key":"S095679682100023X_ref57","doi-asserted-by":"publisher","DOI":"10.1098\/rsta.2015.0404"},{"key":"S095679682100023X_ref103","doi-asserted-by":"publisher","DOI":"10.1109\/FTCS.1990.89397"},{"key":"S095679682100023X_ref111","first-page":"427","volume-title":"Principles of Programming Languages","author":"Zhao","year":"2012"},{"key":"S095679682100023X_ref23","unstructured":"Cheung, L. , O\u2019Connor, L. and Rizkallah, C. (2021) Overcoming restraint: Modular refinement using cogent\u2019s principled foreign function interface. CoRR abs\/2102.09920. Under submission."},{"key":"S095679682100023X_ref41","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)70843-7"},{"key":"S095679682100023X_ref42","doi-asserted-by":"publisher","DOI":"10.1109\/SP.1982.10014"},{"key":"S095679682100023X_ref8","doi-asserted-by":"publisher","DOI":"10.1109\/ISoLA.2006.14"},{"key":"S095679682100023X_ref63","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"S095679682100023X_ref94","doi-asserted-by":"publisher","DOI":"10.1145\/141471.141563"},{"key":"S095679682100023X_ref15","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681300018X"},{"key":"S095679682100023X_ref73","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-06200-6_4"},{"key":"S095679682100023X_ref83","doi-asserted-by":"publisher","DOI":"10.1145\/2541568.2541570"},{"key":"S095679682100023X_ref71","doi-asserted-by":"publisher","DOI":"10.1145\/1065887.1065892"},{"key":"S095679682100023X_ref85","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0055057"},{"key":"S095679682100023X_ref108","unstructured":"Wadler, P. (1990) Linear types can change the world! In Programming Concepts and Methods."},{"key":"S095679682100023X_ref36","first-page":"1","volume-title":"Web Services and Formal Methods","author":"Dezani-Ciancaglini","year":"2010"},{"key":"S095679682100023X_ref107","first-page":"97","volume-title":"Principles of Programming Languages","author":"Tuch","year":"2007"},{"key":"S095679682100023X_ref4","unstructured":"Amani, S. (2016) A Methodology for Trustworthy File Systems. PhD thesis, University of New South Wales."},{"key":"S095679682100023X_ref100","unstructured":"Shang, Z. (2020) An LLVM Backend of the Cogent Compiler. Project report, UNSW Sydney, Computer Science & Engineering."},{"key":"S095679682100023X_ref38","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24725-8_15"},{"key":"S095679682100023X_ref65","doi-asserted-by":"crossref","unstructured":"Maric, O. and Sprenger, C. (2014) Verification of a transactional memory manager under hardware failures and restarts. In International Symposium on Formal Methods. Lecture Notes in Computer Science, vol. 8442. Springer, pp. 449\u2013464.","DOI":"10.1007\/978-3-319-06410-9_31"},{"key":"S095679682100023X_ref84","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0054170"},{"key":"S095679682100023X_ref93","doi-asserted-by":"crossref","unstructured":"Rustan, K. and Leino, M. (2010) Dafny: An automatic program verifier for functional correctness. In Logic for Programming, Artificial Intelligence, and Reasoning. Springer, pp. 348\u2013370.","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"S095679682100023X_ref5","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018627"},{"key":"S095679682100023X_ref109","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806610"},{"key":"S095679682100023X_ref77","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03418-4_9"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S095679682100023X","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T22:36:12Z","timestamp":1779834972000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S095679682100023X\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"references-count":111,"alternative-id":["S095679682100023X"],"URL":"https:\/\/doi.org\/10.1017\/s095679682100023x","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"\u00a9 The Author(s), 2021. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (https:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution, and reproduction in any medium, provided the original work is properly cited.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}],"article-number":"e25"}}