{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,7]],"date-time":"2026-06-07T04:48:52Z","timestamp":1780807732274,"version":"3.54.1"},"reference-count":53,"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":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-2005545"],"award-info":[{"award-number":["CCF-2005545"]}],"id":[{"id":"10.13039\/100000001","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>One can write dependently typed functional programs in Coq, and prove them correct in Coq; one can write low-level programs in C, and prove them correct with a C verification tool. We demonstrate how to write programs partly in Coq and partly in C, and interface the proofs together. The Verified Foreign Function Interface (VeriFFI) guarantees type safety and correctness of the combined program. It works by translating Coq function types (and constructor types) along with Coq functional models into VST function-specifications; if the user can prove in VST that the C functions satisfy those specs, then the C functions behave according to the user-specified functional models (even though the C implementation might be very different) and the proofs of Coq functions that call the C code can rely on that behavior. To achieve this translation, we employ a novel, hybrid deep\/shallow description of Coq dependent types.<\/jats:p>","DOI":"10.1145\/3704860","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"687-717","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["A Verified Foreign Function Interface between Coq and C"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6784-7108","authenticated-orcid":false,"given":"Joomy","family":"Korkut","sequence":"first","affiliation":[{"name":"Princeton University, Princeton, USA"},{"name":"Bloomberg, New York, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7086-6518","authenticated-orcid":false,"given":"Kathrin","family":"Stark","sequence":"additional","affiliation":[{"name":"Heriot-Watt University, Edinburgh, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6009-0325","authenticated-orcid":false,"given":"Andrew W.","family":"Appel","sequence":"additional","affiliation":[{"name":"Princeton University, Princeton, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_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: Third International Workshop on Coq for Programming Languages. 2 pages. https:\/\/www.cs.princeton.edu\/~appel\/papers\/certicoq-coqpl.pdf"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107256552"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3607858"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/146637.146666"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80452-9"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9457-5"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3689786"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3497775.3503686"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1292535.1292541"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3674628"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065019"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_21"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1377492.1377493"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622823"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_22"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535841"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/178243.178246"},{"key":"e_1_3_2_20_1","unstructured":"Xavier Leroy. 1999. CamlIDL user\u2019s manual. https:\/\/caml.inria.fr\/pub\/old_caml_site\/camlidl\/htmlman\/"},{"key":"e_1_3_2_21_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 POPL\u201906: 33rd Annual ACM SIGPLAN-SIGACT Symposium on Principles ofProgramming Languages. 42\u201354. https:\/\/doi.org\/10.1145\/1111037.1111042 10.1145\/1111037.1111042","DOI":"10.1145\/1111037.1111042"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-020-00523-2"},{"key":"e_1_3_2_23_1","volume-title":"Java Native Interface: Programmer\u2019s Guide and Reference","author":"Liang Sheng","year":"1999","unstructured":"Sheng Liang. 1999. Java Native Interface: Programmer\u2019s Guide and Reference. Addison-Wesley Longman."},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/358141.358147"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314622"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190220"},{"key":"e_1_3_2_27_1","volume-title":"The Meaning of Multilanguage Programs","author":"Matthews Jacob Burton","year":"2008","unstructured":"Jacob Burton Matthews. 2008. The Meaning of Multilanguage Programs. Ph. D. Dissertation. The University of Chicago. https:\/\/web.archive.org\/web\/20240331001311\/ https:\/\/plt.cs.northwestern.edu\/matthews-phd.pdf"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863495.1863497"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","unstructured":"Andrew McCreight Tim Chevalier and Andrew Tolmach. 2010. A certified framework for compiling and executing garbage-collected languages. In ICFP\u201910: 15th ACM SIGPLAN International Conference on Functional programming. 273\u2013284. https:\/\/doi.org\/10.1145\/1863543.1863584 10.1145\/1863543.1863584","DOI":"10.1145\/1863543.1863584"},{"key":"e_1_3_2_30_1","unstructured":"Wolfgang Meier Jean Pichon-Pharabod and Bas Spitters. 2024. CertiCoq-Wasm: Verified compilation from Coq to WebAssembly. In CoqPL\u201924: The Tenth International Workshop on Coq for Programming Languages. 3 pages.https:\/\/popl24.sigplan.org\/details\/CoqPL-2024-papers\/3\/CertiCoq-Wasm-Verified-compilation-from-Coq-to-WebAssembly"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2611429.2611829"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1017\/9781009129220"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167089"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2021.29"},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.5555\/580840"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.5555\/AAI28153473"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341687"},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485491"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473591"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_8"},{"key":"e_1_3_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/158511.158524"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237741"},{"key":"e_1_3_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/44546.44559"},{"key":"e_1_3_2_44_1","doi-asserted-by":"publisher","unstructured":"Jacob Prinz G.A. Kavvos and Leonidas Lampropoulos. 2022. Deeper Shallow Embeddings. In International Conference on Interactive Theorem Proving. 18 pages. https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2022.28 10.4230\/LIPIcs.ITP.2022.28","DOI":"10.4230\/LIPIcs.ITP.2022.28"},{"key":"e_1_3_2_45_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2019.102372"},{"key":"e_1_3_2_46_1","doi-asserted-by":"publisher","unstructured":"Olivier Savary B\u00e9langer and Andrew W. Appel. 2017. Shrink Fast Correctly!. In PPDP\u201917: International Symposium on Principles and Practice of Declarative Programming. 49\u201360. https:\/\/doi.org\/10.1145\/3131851.3131859 10.1145\/3131851.3131859","DOI":"10.1145\/3131851.3131859"},{"key":"e_1_3_2_47_1","unstructured":"Olivier Savary B\u00e9langer Matthew Z. Weaver and Andrew W. Appel. 2019. Certified Code Generation from CPS to C. 13 pages. https:\/\/www.cs.princeton.edu\/~appel\/papers\/CPStoC.pdf"},{"key":"e_1_3_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371076"},{"key":"e_1_3_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/1291201.1291206"},{"key":"e_1_3_2_50_1","unstructured":"Gang Tan Andrew W Appel Srimat Chakradhar Anand Raghunathan Srivaths Ravi and Daniel Wang. 2006. Safe Java native interface. In IEEE International Symposium on Secure Software Engineering Vol. 97. 106\u2013119."},{"key":"e_1_3_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/143165.143169"},{"key":"e_1_3_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360597"},{"key":"e_1_3_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371119"},{"key":"e_1_3_2_54_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2017.04.002"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704860","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704860","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:16:43Z","timestamp":1770200203000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704860"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":53,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704860"],"URL":"https:\/\/doi.org\/10.1145\/3704860","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-09","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"}}]}}