{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T23:06:04Z","timestamp":1779836764611,"version":"3.53.1"},"reference-count":64,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2022,8,22]],"date-time":"2022-08-22T00:00:00Z","timestamp":1661126400000},"content-version":"unspecified","delay-in-days":233,"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":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    We implement extraction of Coq programs to functional languages based on MetaCoq\u2019s certified erasure. We extend the MetaCoq erasure output language with typing information and use it as an intermediate representation, which we call\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0956796822000077_inline1.png\"\/>\n                        <jats:tex-math>${\\lambda^T_\\square}$<\/jats:tex-math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    . We complement the extraction functionality with a full pipeline that includes several standard transformations (e.g. eta-expansion and inlining) implemented in a proof-generating manner along with a verified optimisation pass removing unused arguments. We prove the pass correct wrt. a conventional call-by-value operational semantics of functional languages. From the optimised\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0956796822000077_inline2.png\"\/>\n                        <jats:tex-math>${\\lambda^T_\\square}$<\/jats:tex-math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    representation, we obtain code in two functional smart contract languages, Liquidity and CameLIGO, the functional language Elm, and a subset of the multi-paradigm language for systems programming Rust. Rust is currently gaining popularity as a language for smart contracts, and we demonstrate how our extraction can be used to extract smart contract code for the Concordium network. The development is done in the context of the ConCert framework that enables smart contract verification. We contribute with two verified real-world smart contracts (boardroom voting and escrow), which we use, among other examples, to exemplify the applicability of the pipeline. In addition, we develop a verified web application and extract it to fully functional Elm code. In total, this gives us a way to write dependently typed programs in Coq, verify, and then extract them to several target languages while retaining a small trusted computing base of only MetaCoq and the pretty-printers into these languages.\n                  <\/jats:p>","DOI":"10.1017\/s0956796822000077","type":"journal-article","created":{"date-parts":[[2022,8,22]],"date-time":"2022-08-22T05:38:06Z","timestamp":1661146686000},"update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":5,"title":["Extracting functional programs from Coq, in Coq"],"prefix":"10.1017","volume":"32","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8278-3069","authenticated-orcid":false,"given":"DANIL","family":"ANNENKOV","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3261-5205","authenticated-orcid":false,"given":"MIKKEL","family":"MILO","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0459-2678","authenticated-orcid":false,"given":"JAKOB BOTSCH","family":"NIELSEN","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2802-0973","authenticated-orcid":false,"given":"BAS","family":"SPITTERS","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2022,8,22]]},"reference":[{"key":"S0956796822000077_ref55","unstructured":"Prost, F. (1995) Marking techniques for extraction. Research Report LIP RR-1995-47, Laboratoire de l\u2019informatique du parall\u00e9lisme. Available at: https:\/\/hal-lara.archives-ouvertes.fr\/hal-02102062."},{"key":"S0956796822000077_ref15","doi-asserted-by":"publisher","DOI":"10.1002\/spe.4380180902"},{"key":"S0956796822000077_ref59","doi-asserted-by":"crossref","unstructured":"Sozeau, M. , Boulier, S. , Forster, Y. , Tabareau, N. & Winterhalter, T. (2019) Coq Coq Correct! verification of type checking and erasure for Coq, in Coq. In POPL\u20192019.","DOI":"10.1145\/3371076"},{"key":"S0956796822000077_ref60","doi-asserted-by":"publisher","DOI":"10.1145\/3341690"},{"key":"S0956796822000077_ref18","unstructured":"Brady, E. (2021) Idris 2: Quantitative type theory in practice. In 35th European Conference on Object-Oriented Programming (ECOOP 2021), M\u00f8ller, A. & Sridharan, M. (eds). Leibniz International Proceedings in Informatics (LIPIcs), vol. 194. Dagstuhl, Germany: Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, pp. 9:1\u20139:26."},{"key":"S0956796822000077_ref13","unstructured":"Bernardo, B. (2015) Un Calcul des Constructions implicite avec sommes d\u00e9pendantes et \u00c0 inf\u00e9rence de type d\u00e9cidable. Theses, \u00e9cole polytechnique. Version soutenance. Available at: https:\/\/hal.inria.fr\/tel-01197380"},{"key":"S0956796822000077_ref29","doi-asserted-by":"publisher","DOI":"10.1145\/3290316"},{"key":"S0956796822000077_ref22","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.11.024"},{"key":"S0956796822000077_ref12","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45842-5_2"},{"key":"S0956796822000077_ref64","unstructured":"Weiss, A. , Gierczak, O. , Patterson, D. , Matsakis, N. D. & Ahmed, A. (2019) Oxide: The Essence of Rust. arXiv e-prints."},{"key":"S0956796822000077_ref16","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57880-3_8"},{"key":"S0956796822000077_ref20","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-33636-3_10"},{"key":"S0956796822000077_ref37","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535841"},{"key":"S0956796822000077_ref42","doi-asserted-by":"crossref","first-page":"42","DOI":"10.1145\/1111037.1111042","article-title":"Formal certification of a compiler back-end, or: Programming a compiler with a proof assistant","author":"Leroy","year":"2006","journal-title":"POPL"},{"key":"S0956796822000077_ref24","unstructured":"Danielsson, N. A. (2019) Logical properties of a modality for erasure. Accessed July 7, 2021. Available at: http:\/\/www.cse.chalmers.se\/ nad\/publications\/danielsson-erased.pdf."},{"key":"S0956796822000077_ref50","doi-asserted-by":"crossref","unstructured":"Nielsen, J. B. & Spitters, B. (2019) Smart contract interactions in Coq. In FMBC\u20192019.","DOI":"10.1007\/978-3-030-54994-7_29"},{"key":"S0956796822000077_ref61","doi-asserted-by":"publisher","DOI":"10.1145\/3441296.3441394"},{"key":"S0956796822000077_ref63","doi-asserted-by":"publisher","DOI":"10.1145\/3167082"},{"key":"S0956796822000077_ref14","first-page":"157","volume-title":"In PLDI","author":"Boehm","year":"1991"},{"key":"S0956796822000077_ref2","unstructured":"Anand, A. , Appel, A. , Morrisett, G. , Paraskevopoulou, Z. , Pollack, R. , Belanger, O. , Sozeau, M. & Weaver, M. (2017) CertiCoq: A verified compiler for Coq. In CoqPL\u20192017."},{"key":"S0956796822000077_ref34","doi-asserted-by":"publisher","DOI":"10.1145\/3418295"},{"key":"S0956796822000077_ref4","doi-asserted-by":"publisher","DOI":"10.1145\/3236950.3236955"},{"key":"S0956796822000077_ref53","doi-asserted-by":"crossref","unstructured":"Paulin-Mohring, C. (1989) Extracting F $\\omega$ \u2019s programs from proofs in the calculus of constructions. In Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages\u2019, POPL\u201989. New York, NY, USA: Association for Computing Machinery, pp. 89\u2013104.","DOI":"10.1145\/75277.75285"},{"key":"S0956796822000077_ref57","unstructured":"\u0160inkarovs, A. & Cockx, J. (2021) Choosing is Losing: How to combine the benefits of shallow and deep embeddings through reflection."},{"key":"S0956796822000077_ref3","first-page":"20","article-title":"Towards certified meta-programming with typed template-Coq","volume":"10895","author":"Anand","year":"2018","journal-title":"In ITP18. LNCS"},{"key":"S0956796822000077_ref25","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243857"},{"key":"S0956796822000077_ref62","unstructured":"Timany, A. & Sozeau, M. (2017) Consistency of the predicative calculus of cumulative inductive constructions (pCuIC). CoRR abs\/1710.03912. Available at: http:\/\/arxiv.org\/abs\/1710.03912"},{"key":"S0956796822000077_ref8","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784747"},{"key":"S0956796822000077_ref51","volume-title":"Simplicity: A new language for blockchains","author":"O\u2019Connor","year":"2017"},{"key":"S0956796822000077_ref6","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373829"},{"key":"S0956796822000077_ref30","volume-title":"A code generator framework for Isabelle\/HOL","author":"Haftmann","year":"2007"},{"key":"S0956796822000077_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78499-9_26"},{"key":"S0956796822000077_ref38","unstructured":"Kusee, W. H. (2017) Compiling Agda to Haskell with Fewer Coercions. Master\u2019s thesis."},{"key":"S0956796822000077_ref45","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-70972-7_20"},{"key":"S0956796822000077_ref21","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/9153.001.0001"},{"key":"S0956796822000077_ref27","volume-title":"Elm in Action","author":"Feldman","year":"2020"},{"key":"S0956796822000077_ref31","article-title":"Anonymous voting by two-round public discussion","volume":"4","author":"Hao","year":"2010","journal-title":"IET Inf. Security"},{"key":"S0956796822000077_ref32","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-54455-3_42"},{"key":"S0956796822000077_ref40","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/6.4.308"},{"key":"S0956796822000077_ref35","volume-title":"The Rust Programming Language","author":"Klabnik","year":"2018"},{"key":"S0956796822000077_ref43","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-39185-1_12"},{"key":"S0956796822000077_ref39","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03427-6_27"},{"key":"S0956796822000077_ref44","unstructured":"Letouzey, P. (2004) Programmation fonctionnelle certifi\u00e9e \u2013 L\u2019extraction de programmes dans l\u2019assistant Coq. PhD thesis, Universit\u00e9 Paris-Sud. English version: https:\/\/www.irif.fr\/ letouzey\/download\/these_letouzey_English.ps.gz."},{"key":"S0956796822000077_ref54","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51054-1_7"},{"key":"S0956796822000077_ref52","doi-asserted-by":"publisher","DOI":"10.1145\/3473591"},{"key":"S0956796822000077_ref7","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209189"},{"key":"S0956796822000077_ref5","first-page":"105","volume-title":"CPP 2021","author":"Annenkov","year":"2021"},{"key":"S0956796822000077_ref26","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2019.00005"},{"key":"S0956796822000077_ref11","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/6.5.663"},{"key":"S0956796822000077_ref23","doi-asserted-by":"publisher","DOI":"10.1007\/10930755_14"},{"key":"S0956796822000077_ref58","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-019-09540-0"},{"key":"S0956796822000077_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/11538363_12"},{"key":"S0956796822000077_ref28","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24725-8_26"},{"key":"S0956796822000077_ref46","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45413-6_27"},{"key":"S0956796822000077_ref36","doi-asserted-by":"publisher","DOI":"10.1145\/2560537"},{"key":"S0956796822000077_ref49","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263712"},{"key":"S0956796822000077_ref41","doi-asserted-by":"publisher","DOI":"10.1145\/291891.291892"},{"key":"S0956796822000077_ref17","unstructured":"Bozman, c. , Iguernlala, M. , Laporte, M. , Le Fessant, F. & Mebsout, A. (2018) Liquidity: OCaml pour la Blockchain. In JFLA18."},{"key":"S0956796822000077_ref48","doi-asserted-by":"crossref","unstructured":"Mullen, E. , Pernsteiner, S. , Wilcox, J. R. , Tatlock, Z. & Grossman, D. (2018) \u0152uf: Minimizing the Coq extraction TCB. In CPP 2018.","DOI":"10.1145\/3176245.3167089"},{"key":"S0956796822000077_ref47","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78499-9_25"},{"key":"S0956796822000077_ref1","volume-title":"Cryptology ePrint Archive","author":"Abate","year":"2021"},{"key":"S0956796822000077_ref19","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24849-1_8"},{"key":"S0956796822000077_ref56","doi-asserted-by":"publisher","DOI":"10.1145\/3360611"},{"key":"S0956796822000077_ref33","doi-asserted-by":"crossref","first-page":"999","DOI":"10.1007\/978-3-319-89884-1_35","article-title":"A verified compiler from Isabelle\/HOL to CakeML","author":"Hupel","year":"2018","journal-title":"Programming Languages and Systems"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796822000077","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T22:36:59Z","timestamp":1779835019000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796822000077\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"references-count":64,"alternative-id":["S0956796822000077"],"URL":"https:\/\/doi.org\/10.1017\/s0956796822000077","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"\u00a9 The Author(s), 2022. 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":"e11"}}