{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T05:05:23Z","timestamp":1750309523248,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":51,"publisher":"ACM","license":[{"start":{"date-parts":[[2025,1,10]],"date-time":"2025-01-10T00:00:00Z","timestamp":1736467200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,1,10]]},"DOI":"10.1145\/3703595.3705879","type":"proceedings-article","created":{"date-parts":[[2025,1,10]],"date-time":"2025-01-10T21:23:16Z","timestamp":1736544196000},"page":"127-139","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["CertiCoq-Wasm: A Verified WebAssembly Backend for CertiCoq"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0005-3633-2490","authenticated-orcid":false,"given":"Wolfgang","family":"Meier","sequence":"first","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-5027-9249","authenticated-orcid":false,"given":"Martin","family":"Jensen","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4442-6543","authenticated-orcid":false,"given":"Jean","family":"Pichon-Pharabod","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2802-0973","authenticated-orcid":false,"given":"Bas","family":"Spitters","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}]}],"member":"320","published-online":{"date-parts":[[2025,1,10]]},"reference":[{"key":"e_1_3_2_2_1_1","volume-title":"Matthieu Sozeau, and Matthew Weaver.","author":"Anand Abhishek","year":"2017","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 The third international workshop on Coq for programming languages (CoqPL)."},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796822000077"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373829"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2774972"},{"key":"e_1_3_2_2_5_1","unstructured":"Andrew W Appel. 2022. Verified Functional Algorithms (Software Foundations Vol. 3). Electronic textbook (2022)."},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.239.2"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-017-0435-9_2"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9148-3"},{"key":"e_1_3_2_2_9_1","volume-title":"Liquidity: Ocaml pour la blockchain. Journ\u00e9es Francophones des Langages Applicatifs 2018","author":"Bozman \u00c7agdas","year":"2018","unstructured":"\u00c7agdas Bozman, Mohamed Iguernlala, Michael Laporte, FL Fessant, and Alain Mebsout. 2018. Liquidity: Ocaml pour la blockchain. Journ\u00e9es Francophones des Langages Applicatifs 2018 (2018)."},{"key":"e_1_3_2_2_10_1","volume-title":"Appel","author":"B\u00e9langer Olivier Savary","year":"2019","unstructured":"Olivier Savary B\u00e9langer, Matthew Z. Weaver, , and Andrew W. Appel. 2019. Certified Code Generation from CPS to C. Technical Report. Princeton University."},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/0096-0551(81)90048-5"},{"key":"e_1_3_2_2_12_1","unstructured":"Concordium Development Team. 2021. Concordium whitepaper version 1.8.1. https:\/\/go.concordium.com\/hubfs\/White"},{"key":"e_1_3_2_2_13_1","volume-title":"Prakash Panangaden, James T. Sasaki, and Scott F. Smith.","author":"Constable Robert L.","year":"1986","unstructured":"Robert L. Constable, Stuart F. Allen, Mark Bromley, Rance Cleaveland, J. F. Cremer, Robert Harper, Douglas J. Howe, Todd B. Knoblock, Nax Paul Mendler, Prakash Panangaden, James T. Sasaki, and Scott F. Smith. 1986. Implementing mathematics with the Nuprl proof development system. Prentice Hall. isbn:978-0-13-451832-9 https:\/\/nuprl-web.cs.cornell.edu\/book\/"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_26"},{"key":"e_1_3_2_2_15_1","unstructured":"Coq development team. 2023. The Gallina specification language. https:\/\/coq.inria.fr\/doc\/V8.18.0\/refman\/language\/gallina-specification-language.html"},{"key":"e_1_3_2_2_16_1","volume-title":"ML Workshop.","author":"Dolan Stephen","year":"2016","unstructured":"Stephen Dolan. 2016. Malfunctional programming. In ML Workshop."},{"volume-title":"Elm in action","author":"Feldman Richard","key":"e_1_3_2_2_17_1","unstructured":"Richard Feldman. 2020. Elm in action. Manning Publications. isbn:9781617294044"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656379"},{"key":"e_1_3_2_2_19_1","volume-title":"JFLA 2009, Vingti\u00e8mes Journ\u00e9es Francophones des Langages Applicatifs, Saint Quentin sur Is\u00e8re, France, January 31 - February 3, 2009. Proceedings (Studia Informatica Universalis","volume":"7","author":"Glondu St\u00e9phane","year":"2009","unstructured":"St\u00e9phane Glondu. 2009. Extraction certifi\u00e9e dans Coq-en-Coq. In JFLA 2009, Vingti\u00e8mes Journ\u00e9es Francophones des Langages Applicatifs, Saint Quentin sur Is\u00e8re, France, January 31 - February 3, 2009. Proceedings (Studia Informatica Universalis, Vol. 7.2), Alan Schmitt (Ed.). 383\u2013410."},{"volume-title":"Vers une certification de l\u2019extraction de Coq. (Towards certification of the extraction of Coq). Ph. D. Dissertation","author":"Glondu St\u00e9phane","key":"e_1_3_2_2_20_1","unstructured":"St\u00e9phane Glondu. 2012. Vers une certification de l\u2019extraction de Coq. (Towards certification of the extraction of Coq). Ph. D. Dissertation. Paris Diderot University, France."},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062363"},{"key":"e_1_3_2_2_22_1","volume-title":"Verified Code Generation from Isabelle\/HOL. Ph. D. Dissertation","author":"Hupel Lars","year":"2019","unstructured":"Lars Hupel. 2019. Verified Code Generation from Isabelle\/HOL. Ph. D. Dissertation. Technical University of Munich, Germany. https:\/\/nbn-resolving.org\/urn:nbn:de:bvb:91-diss-20190711-1473785-1-3"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_35"},{"key":"e_1_3_2_2_24_1","volume-title":"Proc. ACM Program. Lang. 9, POPL","author":"Korkut Joomy","year":"2025","unstructured":"Joomy Korkut, Kathrin Stark, and Andrew W. Appel. 2025. A Verified Foreign Function Interface Between Coq and C. Proc. ACM Program. Lang. 9, POPL (2025)."},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-39185-1_12"},{"volume-title":"Programmation fonctionnelle certifi\u00e9e : L\u2019extraction de programmes dans l\u2019assistant Coq. (Certified functional programming : Program extraction within Coq proof assistant). Ph. D. Dissertation","author":"Letouzey Pierre","key":"e_1_3_2_2_27_1","unstructured":"Pierre Letouzey. 2004. Programmation fonctionnelle certifi\u00e9e : L\u2019extraction de programmes dans l\u2019assistant Coq. (Certified functional programming : Program extraction within Coq proof assistant). Ph. D. Dissertation. University of Paris-Sud, Orsay, France."},{"key":"e_1_3_2_2_28_1","unstructured":"Lorenz Leutgeb. 2018. Towards Verified Compilation of CakeML to WebAssembly. presented at ViennaJS."},{"key":"e_1_3_2_2_29_1","unstructured":"Wolfgang Meier Jean Pichon-Pharabod and Bas Spitters. 2024. CertiCoq-Wasm: Verified compilation from Coq to WebAssembly. presented at CoqPL\u201924. https:\/\/popl24.sigplan.org\/details\/CoqPL-2024-papers\/3\/CertiCoq-Wasm-Verified-compilation-from-Coq-to-WebAssembly"},{"key":"e_1_3_2_2_30_1","unstructured":"Mozilla. 2024. Mozilla Developper Network: WebAssembly. https:\/\/developer.mozilla.org\/en-US\/docs\/WebAssembly"},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167089"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784764"},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9"},{"volume-title":"Verified Optimizations for Functional Languages. Ph. D. Dissertation","author":"Paraskevopoulou Zoe","key":"e_1_3_2_2_34_1","unstructured":"Zoe Paraskevopoulou. 2020. Verified Optimizations for Functional Languages. Ph. D. Dissertation. Princeton University."},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473591"},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75285"},{"key":"e_1_3_2_2_37_1","volume-title":"Extraction de programmes dans le Calcul des Constructions. (Program Extraction in the Calculus of Constructions). Ph. D. Dissertation","author":"Paulin-Mohring Christine","year":"1825","unstructured":"Christine Paulin-Mohring. 1989. Extraction de programmes dans le Calcul des Constructions. (Program Extraction in the Calculus of Constructions). Ph. D. Dissertation. Paris Diderot University, France. https:\/\/tel.archives-ouvertes.fr\/tel-00431825"},{"key":"e_1_3_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(06)80007-6"},{"key":"e_1_3_2_2_39_1","unstructured":"Andreas Rossberg. 2019. WebAssembly Core Specification W3C Recommendation. Technical Report. W3C. https:\/\/www.w3.org\/TR\/wasm-core-1\/"},{"key":"e_1_3_2_2_40_1","unstructured":"Andreas Rossberg. 2023. WebAssembly Core Specification. Technical Report. W3C. https:\/\/webassembly.github.io\/tail-call\/core\/"},{"volume-title":"Verified Extraction for Coq. Ph. D. Dissertation","author":"B\u00e9langer Olivier Savary","key":"e_1_3_2_2_41_1","unstructured":"Olivier Savary B\u00e9langer. 2019. Verified Extraction for Coq. Ph. D. Dissertation. Princeton University."},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-019-09540-0"},{"key":"e_1_3_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371076"},{"key":"e_1_3_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364527.2364531"},{"key":"e_1_3_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2310.02704"},{"key":"e_1_3_2_2_46_1","doi-asserted-by":"publisher","unstructured":"The Coq Development Team. 2023. The Coq Proof Assistant. 10.5281\/zenodo.8161141","DOI":"10.5281\/zenodo.8161141"},{"key":"e_1_3_2_2_47_1","unstructured":"Jerome Vouillon and contributors. 2010. Wasm_of_ocaml: a fork of Js_of_ocaml which compiles OCaml bytecode to WebAssembly. https:\/\/github.com\/ocaml-wasm\/wasm_of_ocaml"},{"key":"e_1_3_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360597"},{"key":"e_1_3_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-90870-6_4"},{"key":"e_1_3_2_2_50_1","unstructured":"Ashley Williams and contributors. 2018. Wasm-pack: your favourite rust to wasm workflow tool. https:\/\/github.com\/rustwasm\/wasm-pack"},{"key":"e_1_3_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2048147.2048224"}],"event":{"name":"CPP '25: 14th ACM SIGPLAN International Conference on Certified Programs and Proofs","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG"],"location":"Denver CO USA","acronym":"CPP '25"},"container-title":["Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3703595.3705879","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3703595.3705879","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:18:08Z","timestamp":1750295888000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3703595.3705879"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,10]]},"references-count":51,"alternative-id":["10.1145\/3703595.3705879","10.1145\/3703595"],"URL":"https:\/\/doi.org\/10.1145\/3703595.3705879","relation":{},"subject":[],"published":{"date-parts":[[2025,1,10]]},"assertion":[{"value":"2025-01-10","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}