{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,27]],"date-time":"2025-08-27T16:14:35Z","timestamp":1756311275291,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":20,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T00:00:00Z","timestamp":1673395200000},"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":[[2023,1,11]]},"DOI":"10.1145\/3573105.3575685","type":"proceedings-article","created":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T22:27:08Z","timestamp":1673476028000},"page":"290-302","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Formalising Decentralised Exchanges in Coq"],"prefix":"10.1145","author":[{"given":"Eske Hoy","family":"Nielsen","sequence":"first","affiliation":[{"name":"Aarhus University, Denmark"}]},{"given":"Danil","family":"Annenkov","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}]},{"given":"Bas","family":"Spitters","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}]}],"member":"320","published-online":{"date-parts":[[2023,1,11]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3437992.3439934"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796822000077"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373829"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"crossref","unstructured":"Bruno Bernardo Rapha\u00ebl Cauderlier Zhenlei Hu Zhenlei Pesin and Julien Tesson. 2019. Mi-Cho-Coq a framework for certifying Tezos Smart Contracts. FMBC.","DOI":"10.1007\/978-3-030-54994-7_28"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485523"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236784"},{"key":"e_1_3_2_1_7_1","unstructured":"Guillaume Claret. 2018. Program in Coq. Universit\u00e9 Sorbonne Paris Cit\u00e9. https:\/\/hal.inria.fr\/tel-01890983"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"crossref","unstructured":"Thierry Coquand and Christine Paulin. 1990. Inductively defined types. In COLOG-88 Per Martin-L\u00f6f and Grigori Mints (Eds.). 50\u201366.","DOI":"10.1007\/3-540-52335-9_47"},{"key":"e_1_3_2_1_9_1","unstructured":"Kim Grauer Will Kueshner and Henry Updegrave. 2022. Chainalysis 2022 Crypto Crime Report. https:\/\/go.chainalysis.com\/2022-Crypto-Crime-Report.html"},{"volume-title":"Principles of Security and Trust","author":"Grishchenko Ilya","key":"e_1_3_2_1_10_1","unstructured":"Ilya Grishchenko, Matteo Maffei, and Clara Schneidewind. 2018. A Semantic Framework for the Security Analysis of Ethereum Smart Contracts. In Principles of Security and Trust. Springer International Publishing, Cham. 243\u2013269. isbn:978-3-319-89722-6"},{"key":"e_1_3_2_1_11_1","unstructured":"Pierre Letouzey. 2004. Programmation fonctionnelle certifi\u00e9e \u2013 L\u2019extraction de programmes dans l\u2019assistant Coq. Ph. D. Dissertation. Universit\u00e9 Paris-Sud. English version: https:\/\/www.irif.fr\/ letouzey\/download\/these_letouzey_English.ps.gz"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","unstructured":"Loi Luu Duc-Hiep Chu Hrishi Olickel Prateek Saxena and Aquinas Hobor. 2016. Making Smart Contracts Smarter. In CCS16. 254\u2013269. isbn:978-1-4503-4139-4 https:\/\/doi.org\/10.1145\/2976749.2978309 10.1145\/2976749.2978309","DOI":"10.1145\/2976749.2978309"},{"key":"e_1_3_2_1_13_1","volume-title":"Brucker","author":"Marmsoler Diego","year":"2021","unstructured":"Diego Marmsoler and Achim D. Brucker. 2021. A Denotational Semantics of\u00a0Solidity in\u00a0Isabelle\/HOL. In Software Engineering and Formal Methods, Radu Calinescu and Corina S. P\u0103s\u0103reanu (Eds.). Springer International Publishing, Cham. 403\u2013422. isbn:978-3-030-92124-8"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","unstructured":"Jakob Botsch Nielsen and Bas Spitters. 2019. Smart Contract Interactions in Coq. In FMBC. https:\/\/doi.org\/10.1007\/978-3-030-54994-7_29 10.1007\/978-3-030-54994-7_29","DOI":"10.1007\/978-3-030-54994-7_29"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00024"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","unstructured":"Matthieu Sozeau Abhishek Anand Simon Boulier Cyril Cohen Yannick Forster Fabian Kunze Gregory Malecha Nicolas Tabareau and Th\u00e9o Winterhalter. 2020. The MetaCoq Project. Journal of Automated Reasoning 18 Feb issn:1573-0670 https:\/\/doi.org\/10.1007\/s10817-019-09540-0 10.1007\/s10817-019-09540-0","DOI":"10.1007\/s10817-019-09540-0"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","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\u20192019. https:\/\/doi.org\/10.1145\/3371076 10.1145\/3371076","DOI":"10.1145\/3371076"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"crossref","unstructured":"Antal Spector-Zabusky Joachim Breitner Christine Rizkallah and Stephanie Weirich. 2018. Total Haskell is Reasonable Coq. CPP18. ACM 14\u201327. isbn:978-1-4503-5586-5","DOI":"10.1145\/3167092"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984027"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3570639"}],"event":{"name":"CPP '23: 12th ACM SIGPLAN International Conference on Certified Programs and Proofs","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"Boston MA USA","acronym":"CPP '23"},"container-title":["Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3573105.3575685","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3573105.3575685","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:45:38Z","timestamp":1750178738000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3573105.3575685"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,11]]},"references-count":20,"alternative-id":["10.1145\/3573105.3575685","10.1145\/3573105"],"URL":"https:\/\/doi.org\/10.1145\/3573105.3575685","relation":{},"subject":[],"published":{"date-parts":[[2023,1,11]]},"assertion":[{"value":"2023-01-11","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}