{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:14:19Z","timestamp":1775873659836,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":51,"publisher":"ACM","license":[{"start":{"date-parts":[[2021,1,17]],"date-time":"2021-01-17T00:00:00Z","timestamp":1610841600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2021,1,17]]},"DOI":"10.1145\/3437992.3439934","type":"proceedings-article","created":{"date-parts":[[2021,1,20]],"date-time":"2021-01-20T23:11:11Z","timestamp":1611184271000},"page":"105-121","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["Extracting smart contracts tested and verified in Coq"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8278-3069","authenticated-orcid":false,"given":"Danil","family":"Annenkov","sequence":"first","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mikkel","family":"Milo","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jakob Botsch","family":"Nielsen","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bas","family":"Spitters","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2021,1,20]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"CoqPL'","author":"Anand Abhishek","year":"2017","unstructured":"Abhishek Anand , Andrew Appel , Greg Morrisett , Zoe Paraskevopoulou , Randy Pollack , Olivier Belanger , Matthieu Sozeau , and Matthew Weaver . 2017. CertiCoq: A verified compiler for Coq . In CoqPL' 2017 . Abhishek Anand, Andrew Appel, Greg Morrisett, Zoe Paraskevopoulou, Randy Pollack, Olivier Belanger, Matthieu Sozeau, and Matthew Weaver. 2017. CertiCoq: A verified compiler for Coq. In CoqPL' 2017."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236950.3236955"},{"key":"e_1_3_2_1_3_1","volume-title":"Jakob Botsch Nielsen, and Bas Spitters","author":"Annenkov Danil","year":"2020","unstructured":"Danil Annenkov , Mikkel Milo , Jakob Botsch Nielsen, and Bas Spitters . 2020 . Source Code for Paper: Extracting Smart Contracts Tested and Verified in Coq . htps:\/\/doi.org\/10.1145\/3410271 10.1145\/3410271 Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, and Bas Spitters. 2020. Source Code for Paper: Extracting Smart Contracts Tested and Verified in Coq. htps:\/\/doi.org\/10.1145\/3410271"},{"key":"e_1_3_2_1_4_1","volume-title":"Jakob Botsch Nielsen, and Bas Spitters","author":"Annenkov Danil","year":"2020","unstructured":"Danil Annenkov , Jakob Botsch Nielsen, and Bas Spitters . 2020 . ConCert: A Smart Contract Certification Framework in Coq. In CPP ' 2020. htps: \/\/doi.org\/10.1145\/3372885.3373829 10.1145\/3372885.3373829 Danil Annenkov, Jakob Botsch Nielsen, and Bas Spitters. 2020. ConCert: A Smart Contract Certification Framework in Coq. In CPP' 2020. htps: \/\/doi.org\/10.1145\/3372885.3373829"},{"key":"#cr-split#-e_1_3_2_1_5_1.1","unstructured":"Patrick Bahr Jost Berthold and Martin Elsman. 2015. Certified Symbolic Management of Financial Multi-Party Contracts. SIGPLAN Not. ( 2015 ) 13 pages. htps:\/\/doi.org\/10.1145\/2784731.2784747 10.1145\/2784731.2784747"},{"key":"#cr-split#-e_1_3_2_1_5_1.2","doi-asserted-by":"crossref","unstructured":"Patrick Bahr Jost Berthold and Martin Elsman. 2015. Certified Symbolic Management of Financial Multi-Party Contracts. SIGPLAN Not. ( 2015 ) 13 pages. htps:\/\/doi.org\/10.1145\/2784731.2784747","DOI":"10.1145\/2784731.2784747"},{"key":"#cr-split#-e_1_3_2_1_6_1.1","unstructured":"Bruno Barras and Benjamin Gr\u00e9goire. 2005. On the Role of Type Decorations in the Calculus of Inductive Constructions. In CSL. htps: \/\/doi.org\/10.1007\/11538363_12 10.1007\/11538363_12"},{"key":"#cr-split#-e_1_3_2_1_6_1.2","doi-asserted-by":"crossref","unstructured":"Bruno Barras and Benjamin Gr\u00e9goire. 2005. On the Role of Type Decorations in the Calculus of Inductive Constructions. In CSL. htps: \/\/doi.org\/10.1007\/11538363_12","DOI":"10.1007\/11538363_12"},{"key":"e_1_3_2_1_7_1","volume-title":"Highassurance field inversion forpairing-friendly primes. Extended abstract. FMBC","author":"Hvass Bas Spitters","year":"2020","unstructured":"Bas Spitters Benjamin S. Hvass , Diego F. Aranha . 2020. Highassurance field inversion forpairing-friendly primes. Extended abstract. FMBC ' 2020 . Bas Spitters Benjamin S. Hvass, Diego F. Aranha. 2020. Highassurance field inversion forpairing-friendly primes. Extended abstract. FMBC' 2020."},{"key":"e_1_3_2_1_8_1","volume-title":"Types for Proofs and Programs","author":"Berghofer Stefan","unstructured":"Stefan Berghofer and Tobias Nipkow . 2002. Executing Higher Order Logic . In Types for Proofs and Programs , Paul Callaghan, Zhaohui Luo, James McKinna, Robert Pollack, and Robert Pollack (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg , 24-40. htps:\/\/doi.org\/10.1007\/3-540-45842-5_2 10.1007\/3-540-45842-5_2 Stefan Berghofer and Tobias Nipkow. 2002. Executing Higher Order Logic. In Types for Proofs and Programs, Paul Callaghan, Zhaohui Luo, James McKinna, Robert Pollack, and Robert Pollack (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 24-40. htps:\/\/doi.org\/10.1007\/3-540-45842-5_2"},{"key":"e_1_3_2_1_9_1","volume-title":"Fabrice Le Fessant, and Alain Mebsout","author":"Bozman \u00c7agdas","year":"2018","unstructured":"\u00c7agdas Bozman , Mohamed Iguernlala , Michael Laporte , Fabrice Le Fessant, and Alain Mebsout . 2018 . Liquidity : OCaml pour la Blockchain. In JFLA 18. \u00c7agdas Bozman, Mohamed Iguernlala, Michael Laporte, Fabrice Le Fessant, and Alain Mebsout. 2018. Liquidity: OCaml pour la Blockchain. In JFLA18."},{"key":"e_1_3_2_1_10_1","volume-title":"Types for Proofs and Programs","author":"Brady Edwin","unstructured":"Edwin Brady , Conor McBride , and James McKinna . 2004. Inductive Families Need Not Store Their Indices . In Types for Proofs and Programs , Stefano Berardi, Mario Coppo, and Ferruccio Damiani (Eds.). Springer Berlin Heidelberg , 115-129. htps:\/\/doi.org\/10.1007\/978-3-540-24849-1_8 10.1007\/978-3-540-24849-1_8 Edwin Brady, Conor McBride, and James McKinna. 2004. Inductive Families Need Not Store Their Indices. In Types for Proofs and Programs, Stefano Berardi, Mario Coppo, and Ferruccio Damiani (Eds.). Springer Berlin Heidelberg, 115-129. htps:\/\/doi.org\/10.1007\/978-3-540-24849-1_8"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-33636-3_10"},{"key":"#cr-split#-e_1_3_2_1_12_1.1","doi-asserted-by":"crossref","unstructured":"Koen Claessen and John Hughes. 2011. QuickCheck: a lightweight tool for random testing of Haskell programs. Acm sigplan notices 46 4 ( 2011 ) 53-64. htps:\/\/doi.org\/10.1145\/351240.351266 10.1145\/351240.351266","DOI":"10.1145\/1988042.1988046"},{"key":"#cr-split#-e_1_3_2_1_12_1.2","doi-asserted-by":"crossref","unstructured":"Koen Claessen and John Hughes. 2011. QuickCheck: a lightweight tool for random testing of Haskell programs. Acm sigplan notices 46 4 ( 2011 ) 53-64. htps:\/\/doi.org\/10.1145\/351240.351266","DOI":"10.1145\/1988042.1988046"},{"key":"e_1_3_2_1_13_1","volume-title":"A Large-Scale Experiment in Executing Extracted Programs. Electron. Notes Theor. Comput. Sci. ( 2006 ). htps:\/\/doi.org\/10.1016\/j.entcs","author":"Cruz-Filipe Lu\u00eds","year":"2005","unstructured":"Lu\u00eds Cruz-Filipe and Pierre Letouzey . 2006. A Large-Scale Experiment in Executing Extracted Programs. Electron. Notes Theor. Comput. Sci. ( 2006 ). htps:\/\/doi.org\/10.1016\/j.entcs . 2005 . 11.024 10.1016\/j.entcs Lu\u00eds Cruz-Filipe and Pierre Letouzey. 2006. A Large-Scale Experiment in Executing Extracted Programs. Electron. Notes Theor. Comput. Sci. ( 2006 ). htps:\/\/doi.org\/10.1016\/j.entcs. 2005. 11.024"},{"key":"#cr-split#-e_1_3_2_1_14_1.1","doi-asserted-by":"crossref","unstructured":"Lu\u00eds Cruz-Filipe and Bas Spitters. 2003. Program Extraction from Large Proof Developments. In Theorem Proving in Higher Order Logics. htps:\/\/doi.org\/10.1007\/10930755_14 10.1007\/10930755_14","DOI":"10.1007\/10930755_14"},{"key":"#cr-split#-e_1_3_2_1_14_1.2","doi-asserted-by":"crossref","unstructured":"Lu\u00eds Cruz-Filipe and Bas Spitters. 2003. Program Extraction from Large Proof Developments. In Theorem Proving in Higher Order Logics. htps:\/\/doi.org\/10.1007\/10930755_14","DOI":"10.1007\/10930755_14"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243857"},{"key":"e_1_3_2_1_16_1","volume-title":"Without Compromises. In IEEE Symposium on Security and Privacy. htps:\/\/doi.org\/10","author":"Erbsen Andres","year":"2019","unstructured":"Andres Erbsen , Jade Philipoom , Jason Gross , Robert Sloan , and Adam Chlipala . 2019 . Simple High-Level Code for Cryptographic Arithmetic-With Proofs , Without Compromises. In IEEE Symposium on Security and Privacy. htps:\/\/doi.org\/10 .1109\/SP. 2019.00005 10.1109\/SP Andres Erbsen, Jade Philipoom, Jason Gross, Robert Sloan, and Adam Chlipala. 2019. Simple High-Level Code for Cryptographic Arithmetic-With Proofs, Without Compromises. In IEEE Symposium on Security and Privacy. htps:\/\/doi.org\/10.1109\/SP. 2019.00005"},{"key":"e_1_3_2_1_17_1","unstructured":"Richard Feldman. 2020. Elm in Action.  Richard Feldman. 2020. Elm in Action."},{"key":"e_1_3_2_1_18_1","first-page":"370","article-title":"Functors for Proofs and Programs. In Programming Languages and Systems, David Schmidt (Ed.)","author":"Filli\u00e2tre Jean-Christophe","year":"2004","unstructured":"Jean-Christophe Filli\u00e2tre and Pierre Letouzey . 2004 . Functors for Proofs and Programs. In Programming Languages and Systems, David Schmidt (Ed.) . Springer Berlin Heidelberg , 370 - 384 . htps:\/\/doi.org\/10.1007\/ 978-3-540-24725-8_26 Jean-Christophe Filli\u00e2tre and Pierre Letouzey. 2004. Functors for Proofs and Programs. In Programming Languages and Systems, David Schmidt (Ed.). Springer Berlin Heidelberg, 370-384. htps:\/\/doi.org\/10.1007\/ 978-3-540-24725-8_26","journal-title":"Springer Berlin Heidelberg"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3395363.3404366"},{"key":"e_1_3_2_1_20_1","volume-title":"Department of Computer Science","author":"Haftmann Florian","unstructured":"Florian Haftmann and Tobias Nipkow . 2007. A code generator framework for Isabelle\/HOL . In Department of Computer Science , University of Kaiserslautern. Florian Haftmann and Tobias Nipkow. 2007. A code generator framework for Isabelle\/HOL. In Department of Computer Science, University of Kaiserslautern."},{"key":"e_1_3_2_1_21_1","volume-title":"Peter YA Ryan, and Piotr Zieli?ski","author":"Hao Feng","year":"2010","unstructured":"Feng Hao , Peter YA Ryan, and Piotr Zieli?ski . 2010 . Anonymous voting by two-round public discussion. IET Information Security 4, 2 ( 2010 ). htps:\/\/doi.org\/10.1049\/iet-ifs. 2008.0127 10.1049\/iet-ifs Feng Hao, Peter YA Ryan, and Piotr Zieli?ski. 2010. Anonymous voting by two-round public discussion. IET Information Security 4, 2 ( 2010 ). htps:\/\/doi.org\/10.1049\/iet-ifs. 2008.0127"},{"key":"e_1_3_2_1_22_1","volume-title":"Christian Kjaer Larsen, and Agata Murawska","author":"Henglein Fritz","year":"2020","unstructured":"Fritz Henglein , Christian Kjaer Larsen, and Agata Murawska . 2020 . A Formally Verified Static Analysis Framework for Compositional Contracts. In Financial Cryptography and Data Security (FC) . htps: \/\/doi.org\/10.1007\/978-3-030-54455-3_42 10.1007\/978-3-030-54455-3_42 Fritz Henglein, Christian Kjaer Larsen, and Agata Murawska. 2020. A Formally Verified Static Analysis Framework for Compositional Contracts. In Financial Cryptography and Data Security (FC). htps: \/\/doi.org\/10.1007\/978-3-030-54455-3_42"},{"key":"#cr-split#-e_1_3_2_1_23_1.1","doi-asserted-by":"crossref","unstructured":"Lars Hupel and Tobias Nipkow. 2018. A Verified Compiler from Isabelle\/HOL to CakeML. In Programming Languages and Systems Amal Ahmed (Ed.). 999-1026. htps:\/\/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":"#cr-split#-e_1_3_2_1_23_1.2","doi-asserted-by":"crossref","unstructured":"Lars Hupel and Tobias Nipkow. 2018. A Verified Compiler from Isabelle\/HOL to CakeML. In Programming Languages and Systems Amal Ahmed (Ed.). 999-1026. htps:\/\/doi.org\/10.1007\/978-3-319-89884-1_35","DOI":"10.1007\/978-3-319-89884-1_35"},{"key":"e_1_3_2_1_24_1","unstructured":"Bo Jiang Ye Liu and W. K. Chan. 2018. ContractFuzzer: Fuzzing Smart Contracts for Vulnerability Detection. CoRR abs\/ 1807.03932 ( 2018 ). arXiv: 1807.03932 htp:\/\/arxiv.org\/abs\/ 1807.03932  Bo Jiang Ye Liu and W. K. Chan. 2018. ContractFuzzer: Fuzzing Smart Contracts for Vulnerability Detection. CoRR abs\/ 1807.03932 ( 2018 ). arXiv: 1807.03932 htp:\/\/arxiv.org\/abs\/ 1807.03932"},{"key":"#cr-split#-e_1_3_2_1_25_1.1","doi-asserted-by":"crossref","unstructured":"Gerwin Klein June Andronick Kevin Elphinstone Toby Murray Thomas Sewell Rafal Kolanski and Gernot Heiser. 2014. Comprehensive Formal Verification of an OS Microkernel. ACM T. Comput. Syst. 32 1 ( 2014 ) 2 : 1-2 : 70. htps:\/\/doi.org\/10.1145\/2560537 10.1145\/2560537","DOI":"10.1145\/2560537"},{"key":"#cr-split#-e_1_3_2_1_25_1.2","doi-asserted-by":"crossref","unstructured":"Gerwin Klein June Andronick Kevin Elphinstone Toby Murray Thomas Sewell Rafal Kolanski and Gernot Heiser. 2014. Comprehensive Formal Verification of an OS Microkernel. ACM T. Comput. Syst. 32 1 ( 2014 ) 2 : 1-2 : 70. htps:\/\/doi.org\/10.1145\/2560537","DOI":"10.1145\/2560537"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535841"},{"key":"e_1_3_2_1_27_1","unstructured":"W. H. Kusee. 2017. Compiling Agda to Haskell with fewer coercions. Master's thesis.  W. H. Kusee. 2017. Compiling Agda to Haskell with fewer coercions. Master's thesis."},{"key":"e_1_3_2_1_28_1","volume-title":"Marlowe: Financial Contracts on Blockchain. In International Symposium on Leveraging Applications of Formal Methods, Verification and Validation","author":"Seijas Pablo Lamela","year":"2018","unstructured":"Pablo Lamela Seijas and Simon Thompson . 2018 . Marlowe: Financial Contracts on Blockchain. In International Symposium on Leveraging Applications of Formal Methods, Verification and Validation . Industrial Practice, Tiziana Margaria and Bernhard Stefen (Eds.). htps:\/\/doi. org\/10.1007\/978-3-030-03427-6_27 Pablo Lamela Seijas and Simon Thompson. 2018. Marlowe: Financial Contracts on Blockchain. In International Symposium on Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice, Tiziana Margaria and Bernhard Stefen (Eds.). htps:\/\/doi. org\/10.1007\/978-3-030-03427-6_27"},{"key":"#cr-split#-e_1_3_2_1_29_1.1","unstructured":"Oukseh Lee and Kwangkeun Yi. 1998. Proofs about a Folklore LetPolymorphic Type Inference Algorithm. ACM Trans. Program. Lang. Syst. ( 1998 ). htps:\/\/doi.org\/10.1145\/291891.291892 10.1145\/291891.291892"},{"key":"#cr-split#-e_1_3_2_1_29_1.2","unstructured":"Oukseh Lee and Kwangkeun Yi. 1998. Proofs about a Folklore LetPolymorphic Type Inference Algorithm. ACM Trans. Program. Lang. Syst. ( 1998 ). htps:\/\/doi.org\/10.1145\/291891.291892"},{"key":"e_1_3_2_1_30_1","first-page":"42","article-title":"Formal certification of a compiler back-end, or: programming a compiler with a proof assistant","author":"Leroy Xavier","year":"2006","unstructured":"Xavier Leroy . 2006 . Formal certification of a compiler back-end, or: programming a compiler with a proof assistant . In POPL. 42 - 54 . htps: \/\/doi.org\/10.1145\/1111037.1111042 10.1145\/1111037.1111042 Xavier Leroy. 2006. Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In POPL. 42-54. htps: \/\/doi.org\/10.1145\/1111037.1111042","journal-title":"POPL."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-39185-1_12"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-70972-7_20"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167089"},{"key":"e_1_3_2_1_35_1","volume-title":"FMBC'","author":"Nielsen Jakob Botsch","year":"2019","unstructured":"Jakob Botsch Nielsen and Bas Spitters . 2019. Smart Contract Interactions in Coq . In FMBC' 2019 . htps:\/\/doi.org\/10.1007\/978-3-030-54994-7_29 10.1007\/978-3-030-54994-7_29 Jakob Botsch Nielsen and Bas Spitters. 2019. Smart Contract Interactions in Coq. In FMBC' 2019. htps:\/\/doi.org\/10.1007\/978-3-030-54994-7_29"},{"key":"e_1_3_2_1_36_1","volume-title":"Simplicity: A New Language for Blockchains (PLAS17). htps:\/\/doi.org\/10.1145\/3139337.3139340","author":"O'Connor Russell","year":"2017","unstructured":"Russell O'Connor . 2017 . Simplicity: A New Language for Blockchains (PLAS17). htps:\/\/doi.org\/10.1145\/3139337.3139340 10.1145\/3139337.3139340 Russell O'Connor. 2017. Simplicity: A New Language for Blockchains (PLAS17). htps:\/\/doi.org\/10.1145\/3139337.3139340"},{"key":"e_1_3_2_1_37_1","first-page":"325","volume-title":"Foundational PropertyBased Testing. In 6th International Conference on Interactive Theorem Proving (ITP) (Lecture Notes in Computer Science","volume":"9236","author":"Paraskevopoulou Zoe","unstructured":"Zoe Paraskevopoulou , Catalin Hritcu , Maxime D\u00e9n\u00e8s , Leonidas Lampropoulos , and Benjamin C. Pierce . 2015 . Foundational PropertyBased Testing. In 6th International Conference on Interactive Theorem Proving (ITP) (Lecture Notes in Computer Science , Vol. 9236 ), Christian Urban and Xingyuan Zhang (Eds.). Springer , 325 - 343 . htps: \/\/doi.org\/10.1007\/978-3-319-22102-1_22 10.1007\/978-3-319-22102-1_22 Zoe Paraskevopoulou, Catalin Hritcu, Maxime D\u00e9n\u00e8s, Leonidas Lampropoulos, and Benjamin C. Pierce. 2015. Foundational PropertyBased Testing. In 6th International Conference on Interactive Theorem Proving (ITP) (Lecture Notes in Computer Science, Vol. 9236 ), Christian Urban and Xingyuan Zhang (Eds.). Springer, 325-343. htps: \/\/doi.org\/10.1007\/978-3-319-22102-1_22"},{"key":"e_1_3_2_1_38_1","unstructured":"Jack Pettersson and Robert Edstr\u00f6m. 2016. Safer smart contracts through type-driven development. Master's thesis.  Jack Pettersson and Robert Edstr\u00f6m. 2016. Safer smart contracts through type-driven development. Master's thesis."},{"key":"#cr-split#-e_1_3_2_1_39_1.1","doi-asserted-by":"crossref","unstructured":"Cl\u00e9ment Pit-Claudel Peng Wang Benjamin Delaware Jason Gross and Adam Chlipala. 2020. Extensible Extraction of Eficient Imperative Programs with Foreign Functions Manually Managed Memory and Proofs. In Automated Reasoning Nicolas Peltier and Viorica Sofronie-Stokkermans (Eds.). 119-137. htps:\/\/doi.org\/10.1007\/978-3-030-51054-1_7 10.1007\/978-3-030-51054-1_7","DOI":"10.1007\/978-3-030-51054-1_7"},{"key":"#cr-split#-e_1_3_2_1_39_1.2","doi-asserted-by":"crossref","unstructured":"Cl\u00e9ment Pit-Claudel Peng Wang Benjamin Delaware Jason Gross and Adam Chlipala. 2020. Extensible Extraction of Eficient Imperative Programs with Foreign Functions Manually Managed Memory and Proofs. In Automated Reasoning Nicolas Peltier and Viorica Sofronie-Stokkermans (Eds.). 119-137. htps:\/\/doi.org\/10.1007\/978-3-030-51054-1_7","DOI":"10.1007\/978-3-030-51054-1_7"},{"key":"#cr-split#-e_1_3_2_1_40_1.1","unstructured":"Ilya Sergey Vaivaswatha Nagaraj Jacob Johannsen Amrit Kumar Anton Trunov and Ken Chan. 2019. Safer Smart Contract Programming with Scilla. In OOPSLA19. htps:\/\/doi.org\/10.5281\/zenodo.3368504 10.5281\/zenodo.3368504"},{"key":"#cr-split#-e_1_3_2_1_40_1.2","doi-asserted-by":"crossref","unstructured":"Ilya Sergey Vaivaswatha Nagaraj Jacob Johannsen Amrit Kumar Anton Trunov and Ken Chan. 2019. Safer Smart Contract Programming with Scilla. In OOPSLA19. htps:\/\/doi.org\/10.5281\/zenodo.3368504","DOI":"10.1145\/3360611"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-019-09540-0"},{"key":"e_1_3_2_1_42_1","volume-title":"Coq. In POPL'","author":"Sozeau Matthieu","year":"2019","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. In POPL' 2019 . htps:\/\/doi.org\/ 10.1145\/3371076 10.1145\/3371076 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. In POPL' 2019. htps:\/\/doi.org\/ 10.1145\/3371076"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341690"}],"event":{"name":"CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs","location":"Virtual Denmark","acronym":"CPP '21","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3437992.3439934","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3437992.3439934","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:47:19Z","timestamp":1750193239000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3437992.3439934"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,17]]},"references-count":51,"alternative-id":["10.1145\/3437992.3439934","10.1145\/3437992"],"URL":"https:\/\/doi.org\/10.1145\/3437992.3439934","relation":{},"subject":[],"published":{"date-parts":[[2021,1,17]]},"assertion":[{"value":"2021-01-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}