{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,21]],"date-time":"2026-05-21T19:43:04Z","timestamp":1779392584917,"version":"3.53.1"},"publisher-location":"New York, NY, USA","reference-count":25,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,1,20]],"date-time":"2020-01-20T00:00:00Z","timestamp":1579478400000},"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":[[2020,1,20]]},"DOI":"10.1145\/3372885.3373829","type":"proceedings-article","created":{"date-parts":[[2020,1,22]],"date-time":"2020-01-22T13:09:33Z","timestamp":1579698573000},"page":"215-228","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":29,"title":["ConCert: a smart contract certification framework in Coq"],"prefix":"10.1145","author":[{"given":"Danil","family":"Annenkov","sequence":"first","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jakob Botsch","family":"Nielsen","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Bas","family":"Spitters","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2020,1,22]]},"reference":[{"key":"e_1_3_2_1_1_1","first-page":"679","volume-title":"POPL17","author":"Amin Nada","unstructured":"Nada Amin and Tiark Rompf . Type Soundness Proofs with Definitional Interpreters . In POPL17 , pages 666\u2013 679 . ACM, 2017. Nada Amin and Tiark Rompf. Type Soundness Proofs with Definitional Interpreters. In POPL17, pages 666\u2013679. ACM, 2017."},{"key":"e_1_3_2_1_2_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 . 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. CertiCoq: A verified compiler for Coq. In CoqPL, 2017."},{"key":"e_1_3_2_1_3_1","series-title":"LNCS","first-page":"39","volume-title":"ITP18","author":"Anand Abhishek","year":"2018","unstructured":"Abhishek Anand , Simon Boulier , Cyril Cohen , Matthieu Sozeau , and Nicolas Tabareau . Towards Certified Meta-Programming with Typed Template-Coq . In ITP18 , volume 10895 of LNCS , pages 20\u2013 39 , 2018 . Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau, and Nicolas Tabareau. Towards Certified Meta-Programming with Typed Template-Coq. In ITP18, volume 10895 of LNCS, pages 20\u201339, 2018."},{"key":"e_1_3_2_1_4_1","volume-title":"CoqPL18","author":"Anand Abhishek","year":"2018","unstructured":"Abhishek Anand and Greg Morrisett . Revisiting Parametricity : Inductives and Uniformity of Propositions . CoqPL18 , 2018 . Abhishek Anand and Greg Morrisett. Revisiting Parametricity: Inductives and Uniformity of Propositions. CoqPL18, 2018."},{"key":"e_1_3_2_1_5_1","volume-title":"FMBC19","author":"Bernardo Bruno","year":"2019","unstructured":"Bruno Bernardo , Rapha\u00ebl Cauderlier , Zhenlei Hu , Zhenlei Pesin , and Julien Tesson . Mi-Cho-Coq, a framework for certifying Tezos Smart Contracts . FMBC19 , 2019 . Bruno Bernardo, Rapha\u00ebl Cauderlier, Zhenlei Hu, Zhenlei Pesin, and Julien Tesson. Mi-Cho-Coq, a framework for certifying Tezos Smart Contracts. FMBC19, 2019."},{"key":"e_1_3_2_1_6_1","volume-title":"MPC19","author":"Chapman James","year":"2019","unstructured":"James Chapman , Roman Kireev , Chad Nester , and Philip Wadler . System F in Agda , for fun and profit . In MPC19 , 2019 . James Chapman, Roman Kireev, Chad Nester, and Philip Wadler. System F in Agda, for fun and profit. In MPC19, 2019."},{"key":"e_1_3_2_1_7_1","first-page":"297","volume-title":"Christiansen and Edwin Brady. Elaborator Reflection: Extending Idris in Idris. In ICFP","author":"David","year":"2016","unstructured":"David Christiansen and Edwin Brady. Elaborator Reflection: Extending Idris in Idris. In ICFP 2016 , pages 284\u2013 297 . ACM, 2016. David Christiansen and Edwin Brady. Elaborator Reflection: Extending Idris in Idris. In ICFP 2016, pages 284\u2013297. ACM, 2016."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110278"},{"key":"e_1_3_2_1_9_1","volume-title":"A certifying extraction with time bounds from Coq to call-by-value \u03bb-calculus. CoRR, abs\/1904.11818","author":"Forster Yannick","year":"2019","unstructured":"Yannick Forster and Fabian Kunze . A certifying extraction with time bounds from Coq to call-by-value \u03bb-calculus. CoRR, abs\/1904.11818 , 2019 . Yannick Forster and Fabian Kunze. A certifying extraction with time bounds from Coq to call-by-value \u03bb-calculus. CoRR, abs\/1904.11818, 2019."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17164-2_25"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978309"},{"key":"e_1_3_2_1_12_1","volume-title":"FMBC19","author":"Nielsen Jakob Botsch","year":"2019","unstructured":"Jakob Botsch Nielsen and Bas Spitters . Smart Contract Interactions in Coq . FMBC19 , 2019 . Jakob Botsch Nielsen and Bas Spitters. Smart Contract Interactions in Coq. FMBC19, 2019."},{"key":"e_1_3_2_1_13_1","first-page":"120","volume-title":"PLAS17","author":"O\u2019Connor Russell","unstructured":"Russell O\u2019Connor . Simplicity : A New Language for Blockchains . PLAS17 , pages 107\u2013 120 . ACM, 2017. Russell O\u2019Connor. Simplicity: A New Language for Blockchains. PLAS17, pages 107\u2013120. ACM, 2017."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60117-1_20"},{"key":"e_1_3_2_1_15_1","volume-title":"MPC19","author":"Jones Michael Peyton","year":"2019","unstructured":"Michael Peyton Jones , Vasilis Gkoumas , Roman Kireev , Kenneth MacKenzie , Chad Nester , and Philip Wadler . Unraveling recursion: compiling an IR with recursion to System F . In MPC19 , 2019 . Michael Peyton Jones, Vasilis Gkoumas, Roman Kireev, Kenneth MacKenzie, Chad Nester, and Philip Wadler. Unraveling recursion: compiling an IR with recursion to System F. In MPC19, 2019."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1010027404223"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-70278-0_30"},{"key":"e_1_3_2_1_18_1","volume-title":"Scilla: a Smart Contract Intermediate-Level LAnguage. CoRR, abs\/1801.00687","author":"Sergey Ilya","year":"2018","unstructured":"Ilya Sergey , Amrit Kumar , and Aquinas Hobor . Scilla: a Smart Contract Intermediate-Level LAnguage. CoRR, abs\/1801.00687 , 2018 . Ilya Sergey, Amrit Kumar, and Aquinas Hobor. Scilla: a Smart Contract Intermediate-Level LAnguage. CoRR, abs\/1801.00687, 2018."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360611"},{"key":"e_1_3_2_1_20_1","first-page":"252","volume-title":"Types for Proofs and Programs","author":"Sozeau Matthieu","unstructured":"Matthieu Sozeau . Subset coercions in Coq . In Thorsten Altenkirch and Conor McBride, editors, Types for Proofs and Programs , pages 237\u2013 252 . Springer Berlin Heidelberg, 2007. Matthieu Sozeau. Subset coercions in Coq. In Thorsten Altenkirch and Conor McBride, editors, Types for Proofs and Programs, pages 237\u2013252. Springer Berlin Heidelberg, 2007."},{"key":"e_1_3_2_1_21_1","first-page":"27","volume-title":"CPP18","author":"Spector-Zabusky Antal","unstructured":"Antal Spector-Zabusky , Joachim Breitner , Christine Rizkallah , and Stephanie Weirich . Total Haskell is Reasonable Coq . CPP18 , pages 14\u2013 27 . ACM, 2018. Antal Spector-Zabusky, Joachim Breitner, Christine Rizkallah, and Stephanie Weirich. Total Haskell is Reasonable Coq. CPP18, pages 14\u201327. ACM, 2018."},{"key":"e_1_3_2_1_22_1","volume-title":"Proc. ACM Program. Lang., 2(ICFP):92:1\u201392:29","author":"Tabareau Nicolas","year":"2018","unstructured":"Nicolas Tabareau , \u00c9ric Tanter , and Matthieu Sozeau. Equivalences for Free: Univalent Parametricity for Effective Transport . Proc. ACM Program. Lang., 2(ICFP):92:1\u201392:29 , July 2018 . Nicolas Tabareau, \u00c9ric Tanter, and Matthieu Sozeau. Equivalences for Free: Univalent Parametricity for Effective Transport. Proc. ACM Program. Lang., 2(ICFP):92:1\u201392:29, July 2018."},{"key":"e_1_3_2_1_23_1","first-page":"173","volume-title":"Implementation and Application of Functional Languages","author":"van der Walt Paul","unstructured":"Paul van der Walt and Wouter Swierstra . Engineering proof by reflection in Agda . In Ralf Hinze, editor, Implementation and Application of Functional Languages , pages 157\u2013 173 . Springer, 2013. Paul van der Walt and Wouter Swierstra. Engineering proof by reflection in Agda. In Ralf Hinze, editor, Implementation and Application of Functional Languages, pages 157\u2013173. Springer, 2013."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3156695.3122963"},{"key":"e_1_3_2_1_25_1","first-page":"286","volume-title":"ICFP13","author":"Weirich Stephanie","unstructured":"Stephanie Weirich , Justin Hsu , and Richard A. Eisenberg . System fc with explicit kind equality . In ICFP13 , pages 275\u2013 286 . ACM, 2013. Stephanie Weirich, Justin Hsu, and Richard A. Eisenberg. System fc with explicit kind equality. In ICFP13, pages 275\u2013286. ACM, 2013."}],"event":{"name":"POPL '20: 47th Annual ACM SIGPLAN Symposium on Principles of Programming Languages","location":"New Orleans LA USA","acronym":"POPL '20","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation"]},"container-title":["Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3372885.3373829","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3372885.3373829","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:41:09Z","timestamp":1750200069000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3372885.3373829"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,1,20]]},"references-count":25,"alternative-id":["10.1145\/3372885.3373829","10.1145\/3372885"],"URL":"https:\/\/doi.org\/10.1145\/3372885.3373829","relation":{},"subject":[],"published":{"date-parts":[[2020,1,20]]},"assertion":[{"value":"2020-01-22","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}