{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T10:07:34Z","timestamp":1781258854954,"version":"3.54.1"},"reference-count":38,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T00:00:00Z","timestamp":1718841600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100018694","name":"HORIZON EUROPE Marie Sklodowska-Curie Actions","doi-asserted-by":"publisher","award":["101024493"],"award-info":[{"award-number":["101024493"]}],"id":[{"id":"10.13039\/100018694","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":[[2024,6,20]]},"abstract":"<jats:p>\n            One of the central claims of fame of the C\n            <jats:sc>oq<\/jats:sc>\n            proof assistant is extraction, i.e., the ability to obtain efficient programs in industrial programming languages such as OC\n            <jats:sc>aml<\/jats:sc>\n            , Haskell, or Scheme from programs written in Coq\u2019s expressive dependent type theory. Extraction is of great practical usefulness, used crucially\n            <jats:italic toggle=\"yes\">e.g.<\/jats:italic>\n            , in the CompCert project. However, for such executables obtained by extraction, the extraction process is part of the trusted code base (TCB), as are Coq\u2019s kernel and the compiler used to compile the extracted code. The extraction process contains intricate semantic transformation of programs that rely on subtle operational features of both the source and target language. Its code has also evolved since the last theoretical exposition in the seminal PhD thesis of Pierre Letouzey. Furthermore, while the exact correctness statements for the execution of extracted code are described clearly in academic literature, the interoperability with unverified code has never been investigated formally, and yet is used in virtually every project relying on extraction. In this paper, we describe the development of a novel extraction pipeline from C\n            <jats:sc>oq<\/jats:sc>\n            to OC\n            <jats:sc>aml<\/jats:sc>\n            , implemented and verified in C\n            <jats:sc>oq<\/jats:sc>\n            itself, with a clear correctness theorem and guarantees for safe interoperability. We build our work on the M\n            <jats:sc>eta<\/jats:sc>\n            Coq project, which aims at decreasing the TCB of Coq\u2019s kernel by re-implementing it in C\n            <jats:sc>oq<\/jats:sc>\n            itself and proving it correct w.r.t. a formal specification of Coq\u2019s type theory in Coq. Since OC\n            <jats:sc>aml<\/jats:sc>\n            does not have a formal specification, we make use of the M\n            <jats:sc>alfunction<\/jats:sc>\n            project specifying the semantics of the intermediate language of the OC\n            <jats:sc>aml<\/jats:sc>\n            compiler. Our work fills some gaps in the literature and highlights important differences between the operational semantics of C\n            <jats:sc>oq<\/jats:sc>\n            programs and their extraction. In particular, we focus on the guarantees that can be provided for interoperability with unverified code, and prove that extracted programs of first-order data type are correct and can safely interoperate, whereas for higher-order programs already simple interoperations can lead to incorrect behaviour and even outright segfaults.\n          <\/jats:p>\n          <jats:p>\n            CCS Concepts:\n            <jats:bold>\u2022 Software and its engineering \u2192 Compilers; Functional languages; Formal software verification; \u2022 Theory of computation \u2192 Type theory.<\/jats:bold>\n          <\/jats:p>","DOI":"10.1145\/3656379","type":"journal-article","created":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T16:27:20Z","timestamp":1718900840000},"page":"52-75","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["Verified Extraction from Coq to OCaml"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8676-9819","authenticated-orcid":false,"given":"Yannick","family":"Forster","sequence":"first","affiliation":[{"name":"Inria, Rennes, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6452-8806","authenticated-orcid":false,"given":"Matthieu","family":"Sozeau","sequence":"additional","affiliation":[{"name":"Inria, Rennes, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3366-2273","authenticated-orcid":false,"given":"Nicolas","family":"Tabareau","sequence":"additional","affiliation":[{"name":"Inria, Rennes, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,6,20]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-020-09559-8"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","unstructured":"Oskar Abrahamsson Magnus O Myreen Ramana Kumar and Thomas Sewell . 2022 Candle: A Verified Implementation of HOL Light. (2022). https:\/\/doi.org\/10.17863\/CAM.84121 10.17863\/CAM.84121","DOI":"10.17863\/CAM.84121"},{"key":"e_1_3_1_4_1","unstructured":"Abhishek Anand Andrew Appel Greg Morrisett Zoe Paraskevopoulou Randy Pollack Olivier Savary Belanger Matthieu Sozeau and Matthew Weaver. 2017 CertiCoq: A verified compiler for Coq. In CoqPL. Paris France. http:\/\/conf.researchr.org\/event\/CoqPL-2017\/main-certicoq-a-verified-compiler-for-coq"},{"key":"e_1_3_1_5_1","unstructured":"Danil Annenkov Mikkel Milo and Bas Spitters. 2021. Code Extraction from Coq to ML-like languages. In ML Family Workshop 2021. https:\/\/github.com\/AU-COBRA\/ConCert\/blob\/master\/papers\/ML-family.pdf"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373829"},{"key":"e_1_3_1_7_1","unstructured":"Andrew Appel Yannick Forster Anvay Grover Joomy Korkut John Li Zoe Paraskevopoulou Kathrin Stark and Matthieu Sozeau. 2022. CertiCoq (GitHub repository). (2022). https:\/\/certicoq.github.io"},{"key":"e_1_3_1_8_1","unstructured":"Andrew W. Appel. 2023. Verified Functional Algorithms. https:\/\/softwarefoundations.cis.upenn.edu\/vfa-current\/index.html Version 1.5.4."},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","unstructured":"Andrew W. Appel and Xavier Leroy. 2023. Efficient Extensional Binary Tries. Journal of Automated Reasoning 67 (2023) article 8. https:\/\/doi.org\/10.1007\/s10817-022-09655-x 10.1007\/s10817-022-09655-x","DOI":"10.1007\/s10817-022-09655-x"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","unstructured":"Martin Bodin Arthur Chargueraud Daniele Filaretti Philippa Gardner Sergio Maffeis Daiva Naudziuniene Alan Schmitt and Gareth Smith. 2014. A Trusted Mechanised JavaScript Specification. SIGPLAN Not. 49 1 (jan 2014) 87\u2013100 https:\/\/doi.org\/10.1145\/2578855.2535876 10.1145\/2578855.2535876","DOI":"10.1145\/2578855.2535876"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062358"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","unstructured":"Edwin C. Brady. 2021. Idris 2: Quantitative Type Theory in Practice. In 35th European Conference on Object-Oriented Programming ECOOP 2021 July 11-17 2021 Aarhus Denmark (Virtual Conference) (LIPIcs Vol. 194) Anders M\u2298ller and Manu Sridharan (Eds.). Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik 9:1\u20139:26. https:\/\/doi.org\/10.4230\/LIPICS.ECOOP.2021.9 10.4230\/LIPICS.ECOOP.2021.9","DOI":"10.4230\/LIPICS.ECOOP.2021.9"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","unstructured":"Gregory J Chaitin Marc A Auslander Ashok K Chandra John Cocke Martin E Hopkins and Peter W Markstein. 1981 Register allocation via coloring. Computer languages 6 1 (1981) 47\u201357. https:\/\/doi.org\/10.1016\/0096-0551(81)90048-5 10.1016\/0096-0551(81)90048-5","DOI":"10.1016\/0096-0551(81)90048-5"},{"key":"e_1_3_1_14_1","doi-asserted-by":"crossref","unstructured":"Cyril Cohen Enzo Crance and Assia Mahboubi. 2024. Trocq: Proof Transfer for Free With or Without Univalence. In ESOP (Lecture Notes in Computer Science Vol. 14576). Springer 239\u2013268.","DOI":"10.1007\/978-3-031-57262-3_10"},{"key":"e_1_3_1_15_1","unstructured":"Stephen Dolan. 2016. Malfunctional programming. In ML Family Workshop 2016. https:\/\/stedolan.net\/talks\/2016\/malfunction\/malfunction.pdf"},{"key":"e_1_3_1_16_1","article-title":"The Type Soundness Theorem That You Really Want to Prove (and Now You Can)","author":"Dreyer Derek","year":"2018","unstructured":"Derek Dreyer. 2018. The Type Soundness Theorem That You Really Want to Prove (and Now You Can). Milner Award Lecture at POPL 2018. https:\/\/www.youtube.com\/watch?v=8Xyk_dGcAwk","journal-title":"Milner Award Lecture at POPL"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","unstructured":"R. Kent Dybvig. 2006. The development of Chez Scheme. In Proceedings of the eleventh ACM SIGPLAN international conference on Functional programming (ICFP06). ACM. https:\/\/doi.org\/10.1145\/1159803.1159805 10.1145\/1159803.1159805","DOI":"10.1145\/1159803.1159805"},{"key":"e_1_3_1_18_1","unstructured":"Yannick Forster and Matthieu Sozeau. 2022. Aspects of a machine-checked intermediate language for extraction from Coq in MetaCoq. In 28th International Conference on Types for Proofs and Programs TYPES 2022 June 2022 20\u201325 Nantes France. https:\/\/types22.inria.fr\/files\/2022\/06\/TYPES_2022_paper_67.pdf"},{"key":"e_1_3_1_19_1","unstructured":"Yannick Forster Matthieu Sozeau Pierre Giraud Pierre-Marie P\u00e9drot and Nicolas Tabareau. 2022. Extraction to OCaml from Coq: Operational Correctness Verified in Coq. In ML Family Workshop 2022. https:\/\/icfp22.sigplan.org\/details\/mlfamilyworkshop-2022-papers\/9\/Extraction-to-OCaml-from-Coq-Operational-Correctness-Verified-in-Coq"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","unstructured":"Lars Hupel and Tobias Nipkow. 2018. A verified compiler from Isabelle\/HOL to CakeML. In European Symposium on Programming. Springer 999\u20131026. https:\/\/doi.org\/10.1007\/978-3-319-89884-1_35 10.1007\/978-3-319-89884-1_35","DOI":"10.1007\/978-3-319-89884-1_35"},{"key":"e_1_3_1_21_1","unstructured":"Jane Street. 2024. Core_bench library. https:\/\/github.com\/janestreet\/core_bench\/"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","unstructured":"Ramana Kumar Magnus O. Myreen Michael Norrish and Scott Owens. 2014. CakeML: A Verified Implementation of ML. In Principles of Programming Languages (POPL). ACM Press 179\u2013191. https:\/\/doi.org\/10.1145\/2535838.2535841 10.1145\/2535838.2535841","DOI":"10.1145\/2535838.2535841"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ITP.2019.22"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/291891.291892"},{"key":"e_1_3_1_25_1","author":"Lennon-Bertrand Meven","year":"2022","unstructured":"Meven Lennon-Bertrand. 2022. \u00c0 bas l' \u03b7 \u2013 Coq's troublesome \u03b7-conversion. In The first Workshop on the Implementation of Type Systems (WITS). https:\/\/www.meven.ac\/documents\/22-WITS-abstract.pdf","journal-title":"In The first Workshop on the Implementation of Type Systems (WITS)."},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","unstructured":"Xavier Leroy. 2006. Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In 33rd symposium Principles of Programming Languages. ACM Press 42\u201354. https:\/\/doi.org\/10.1145\/1111037.1111042 10.1145\/1111037.1111042","DOI":"10.1145\/1111037.1111042"},{"key":"e_1_3_1_27_1","unstructured":"Pierre Letouzey. 2004. Programmation fonctionnelle certifi\u00e9e: l'extraction de programmes dans l'assistant Coq. Th\u00e8se de Doctorat. Universit\u00e9 Paris-Sud. http:\/\/www.pps.jussieu.fr\/letouzey\/download\/these_letouzey.pdf"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-79876-5_37"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","unstructured":"Eric Mullen Stuart Pernsteiner James R. Wilcox Zachary Tatlock and Dan Grossman. 2018. Euf: minimizing the Coq extraction TCB. In Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs CPP 2018 Los Angeles CA USA January 8-9 2018 June Andronick and Amy P. Felty (Eds.). ACM 172\u2013185. https:\/\/doi.org\/10.1145\/3167089 10.1145\/3167089","DOI":"10.1145\/3167089"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","unstructured":"Magnus O. Myreen and Scott Owens. 2012. Proof-producing synthesis of ML from higher-order logic. In Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming (Copenhagen Denmark) (ICFP '12). Association for Computing Machinery New York NY USA 115\u2013126. https:\/\/doi.org\/10.1145\/2364527.2364545 10.1145\/2364527.2364545","DOI":"10.1145\/2364527.2364545"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1017\/s0956796813000282"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","unstructured":"Tobias Nipkow and Simon Ro\u00dfkopf. 2021. Isabelle's Metalogic: Formalization and Proof Checker. Springer International Publishing 93\u2013110. https:\/\/doi.org\/10.1007\/978-3-030-79876-5_6 10.1007\/978-3-030-79876-5_6","DOI":"10.1007\/978-3-030-79876-5_6"},{"key":"e_1_3_1_33_1","unstructured":"Zoe Paraskevopoulou. 2020. Verified Optimizations for Functional Languages. Ph. D. Dissertation. USA. Advisor(s) Appel Andrew. https:\/\/dataspace.princeton.edu\/handle\/88435\/dsp01pr76f648c"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","unstructured":"F. Pfenning and C. Elliott. 1988. Higher-order abstract syntax. ACM SIGPLAN Notices 23 7 (June 1988) 199\u2013208. https:\/\/doi.org\/10.1145\/960116.54010 10.1145\/960116.54010","DOI":"10.1145\/960116.54010"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","unstructured":"Cl\u00e9ment Pit-Claudel Jade Philipoom Dustin Jamner Andres Erbsen and Adam Chlipala. 2022. Relational compilation for performance-critical applications: extensible proof-producing translation of functional models into low-level code. In PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation San Diego CA USA June 13 \u2013 17 2022 Ranjit Jhala and Isil Dillig (Eds.). ACM 918\u2013933. https:\/\/doi.org\/10.1145\/3519939.3523706 10.1145\/3519939.3523706","DOI":"10.1145\/3519939.3523706"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","unstructured":"Jonathan Protzenko Jean-Karim Zinzindohou\u00e9 Aseem Rastogi Tahina Ramananandro Peng Wang Santiago ZanellaB\u00e9guelin Antoine Delignat-Lavaud C\u0103t\u0103lin Hri\u0163cu Karthikeyan Bhargavan C\u00e9dric Fournet and Nikhil Swamy. 2017. Verified low-level programming embedded in F*. Proceedings of the ACM on Programming Languages 1 ICFP (Aug. 2017) 1\u201329. https:\/\/doi.org\/10.1145\/3110261 10.1145\/3110261","DOI":"10.1145\/3110261"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","unstructured":"Matthieu Sozeau Simon Boulier Yannick Forster Nicolas Tabareau and Th\u00e9o Winterhalter. 2019. Coq Coq correct! Verification of type checking and erasure for Coq in Coq. Proceedings of the ACM on Programming Languages 4 POPL (2019) 1\u201328. https:\/\/doi.org\/10.1145\/3371076 10.1145\/3371076","DOI":"10.1145\/3371076"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2398856.2364531"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/359460.359478"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656379","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3656379","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:42:40Z","timestamp":1751661760000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656379"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,20]]},"references-count":38,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2024,6,20]]}},"alternative-id":["10.1145\/3656379"],"URL":"https:\/\/doi.org\/10.1145\/3656379","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,6,20]]},"assertion":[{"value":"2024-06-20","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}