{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,29]],"date-time":"2024-10-29T09:46:09Z","timestamp":1730195169808,"version":"3.28.0"},"reference-count":48,"publisher":"IEEE","license":[{"start":{"date-parts":[[2023,9,16]],"date-time":"2023-09-16T00:00:00Z","timestamp":1694822400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2023,9,16]],"date-time":"2023-09-16T00:00:00Z","timestamp":1694822400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023,9,16]]},"DOI":"10.1109\/aibthings58340.2023.10292478","type":"proceedings-article","created":{"date-parts":[[2023,10,30]],"date-time":"2023-10-30T18:51:40Z","timestamp":1698691900000},"page":"1-10","source":"Crossref","is-referenced-by-count":0,"title":["A model of Solidity-style smart contracts in the theorem prover Agda"],"prefix":"10.1109","author":[{"given":"Fahad","family":"Alhabardi","sequence":"first","affiliation":[{"name":"Swansea University,Department of Computer Science,Swansea,United Kingdom"}]},{"given":"Anton","family":"Setzer","sequence":"additional","affiliation":[{"name":"Swansea University,Department of Computer Science,Swansea,United Kingdom"}]}],"member":"263","reference":[{"article-title":"Ethereum: A next-generation smart contract and decentralized application platform","year":"0","author":"buterin","key":"ref13"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03044-5_5"},{"journal-title":"Mastering Bitcoin Programming the Open Blockchain","year":"2017","author":"antonopoulos","key":"ref12"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-43725-1_11"},{"article-title":"A model of the Solidity-style smart contracts in the theorem prover Agda","year":"2023","author":"setzer","key":"ref15"},{"journal-title":"Intuitionistic type theory","year":"1984","author":"martin-l\u00f6f","key":"ref37"},{"year":"0","key":"ref14","article-title":"Welcome to Agda’s documentation!"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1145\/2841316"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1145\/3360611"},{"article-title":"Vyper documentation","year":"0","author":"team","key":"ref30"},{"key":"ref11","first-page":"107","article-title":"Simplicity: A New Language for Blockchains","author":"o\u2019connor","year":"0"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-31500-9_15"},{"year":"0","key":"ref10","article-title":"Welcome to Liquidity’s documentation"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-06859-7_148"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1109\/iGETblockchain56591.2022.10087054"},{"key":"ref1","first-page":"1:1","article-title":"Verification of Bitcoin Script in Agda Using Weakest Preconditions for Access Control","volume":"239","author":"alhabardi","year":"0"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5"},{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_6"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-54994-7_29"},{"key":"ref38","first-page":"62","article-title":"Verifying Haskell Programs Using Constructive Type Theory","author":"abel","year":"0"},{"journal-title":"Haskell The Craft of Functional Programming","year":"2008","author":"thompson","key":"ref19"},{"year":"0","key":"ref18","article-title":"The Coq Proof Assistants"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2019.00133"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSPW.2018.00013"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-70278-0_28"},{"year":"0","key":"ref45","article-title":"PROOF-OF-STAKE (POS)"},{"key":"ref26","volume":"10001","author":"ahrendt","year":"2016","journal-title":"Deductive Software Verification - The KeY Book - From Theory to Practice"},{"article-title":"Ethereum: A secure decentralised generalised transaction ledger","year":"0","author":"wood","key":"ref48"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-31517-7_16"},{"key":"ref47","first-page":"1","article-title":"Blockchain technology, Bitcoin, and Ethereum: A brief overview","author":"vuji?i?","year":"0"},{"year":"0","key":"ref20","article-title":"OCaml– functional programming language"},{"article-title":"Compiler","year":"0","author":"documentation","key":"ref42"},{"key":"ref41","first-page":"1","article-title":"Relative monads formalised","volume":"7","author":"altenkirch","year":"2014","journal-title":"Journal of Formalized Reasoning"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2021.100665"},{"article-title":"MAlonzo compiler","year":"0","author":"wiki","key":"ref44"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03592-1_13"},{"article-title":"A compiler for Agda","year":"0","author":"benke","key":"ref43"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1145\/3274694.3274743"},{"article-title":"Whylson: Proving your michelson smart contracts in why3","year":"2020","author":"da horta","key":"ref27"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1145\/3395363.3404366"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54455-6_8"},{"key":"ref7","article-title":"Modelling Bitcoin in Agda","volume":"abs 1804 6398","author":"setzer","year":"2018","journal-title":"CoRR"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1016\/j.pmcj.2020.101227"},{"key":"ref4","first-page":"28","article-title":"Smart Contracts: Building Blocks for Digital Markets","volume":"18","author":"szabo","year":"1996","journal-title":"EXTROPY The Journal of Transhumanist Thought"},{"article-title":"Solidity documentation","year":"0","author":"community","key":"ref3"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/ICCCNT.2018.8494045"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1016\/j.future.2019.12.019"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24452-0_5"}],"event":{"name":"2023 IEEE International Conference on Artificial Intelligence, Blockchain, and Internet of Things (AIBThings)","start":{"date-parts":[[2023,9,16]]},"location":"Mount Pleasant, MI, USA","end":{"date-parts":[[2023,9,17]]}},"container-title":["2023 IEEE International Conference on Artificial Intelligence, Blockchain, and Internet of Things (AIBThings)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/10292429\/10291015\/10292478.pdf?arnumber=10292478","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,11,27]],"date-time":"2023-11-27T19:23:00Z","timestamp":1701112980000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/10292478\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,9,16]]},"references-count":48,"URL":"https:\/\/doi.org\/10.1109\/aibthings58340.2023.10292478","relation":{},"subject":[],"published":{"date-parts":[[2023,9,16]]}}}