{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T06:34:32Z","timestamp":1768286072248,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":42,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,12,15]],"date-time":"2023-12-15T00:00:00Z","timestamp":1702598400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,12,15]]},"DOI":"10.1145\/3651655.3651656","type":"proceedings-article","created":{"date-parts":[[2024,5,29]],"date-time":"2024-05-29T16:13:56Z","timestamp":1716999236000},"page":"1-11","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["A simulator of Solidity-style smart contracts in the theorem prover Agda"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0992-2709","authenticated-orcid":false,"given":"Fahad","family":"Alhabardi","sequence":"first","affiliation":[{"name":"Department of Computer Science, Swansea University, United Kingdom"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5322-6060","authenticated-orcid":false,"given":"Anton","family":"Setzer","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Swansea University, United Kingdom"}]}],"member":"320","published-online":{"date-parts":[[2024,5,29]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796816000319"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796816000319"},{"key":"e_1_3_2_1_3_1","volume-title":"Welcome to Agda\u2019s documentation!Retrieved","author":"Community Agda","year":"2023","unstructured":"Agda Community. 2005. Welcome to Agda\u2019s documentation!Retrieved 19 June 2023, Availabe from https:\/\/agda.readthedocs.io\/en\/v2.6.2\/."},{"key":"e_1_3_2_1_4_1","unstructured":"Agda Wiki. 2011. MAlonzo. Retrieved 19 June 2023 Availabe from http:\/\/wiki.portal.chalmers.se\/agda\/pmwiki.php?n=Docs.MAlonzo."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/iGETblockchain56591.2022.10087054"},{"key":"e_1_3_2_1_6_1","volume-title":"August","author":"Alhabardi Fahad","year":"2023","unstructured":"Fahad Alhabardi and Anton Setzer. 2023. A model of Solidity style smart contracts in the theorem prover Agda. https:\/\/fahad1985lab.github.io\/papers\/A_model_of_Solidity-style_smart_contracts_in_the_theorem_prover_Agda.pdf To appear in: To appear in: The IEEE International Conference on Artificial Intelligence, Blockchain, and Internet of Things, (AIBThings), August 2023. Availabe from https:\/\/fahad1985lab.github.io\/papers\/A_model_of_Solidity-style_smart_contracts_in_the_theorem_prover_Agda.pdf."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.TYPES.2021.1"},{"key":"e_1_3_2_1_8_1","volume-title":"Alhabardi and Anton Setzer","author":"F.","year":"2023","unstructured":"Fahad\u00a0F. Alhabardi and Anton Setzer. 2023. Appendix to \u201cA simulator of Solidity-style smart contracts in the theorem prover Agda\u201d., 4\u00a0pages. Available from https:\/\/github.com\/fahad1985lab\/A_simulator_of_Solidity-style_smart_contracts_in_the_theorem_prover_Agda and https:\/\/csetzer.github.io\/articles\/Appendix_to_a_simulator_of_Solidity-style_smart_contracts_in_the_theorem_prover_Agda.pdf."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.pmcj.2020.101227"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/Blockchain.2019.00059"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_6"},{"key":"e_1_3_2_1_13_1","volume-title":"Ethereum: A next-generation smart contract and decentralized application platform. Retrieved","author":"Buterin Vitalik","year":"2014","unstructured":"Vitalik Buterin. 2014. Ethereum: A next-generation smart contract and decentralized application platform. Retrieved 19 June 2023, Availabe from https:\/\/ethereum.org\/en\/whitepaper."},{"key":"e_1_3_2_1_14_1","volume-title":"The Coq Proof Assistants. Retrieved","author":"Community Coq","year":"2023","unstructured":"Coq Community. 2023. The Coq Proof Assistants. Retrieved 15 June 2023, Availabe from https:\/\/coq.inria.fr\/."},{"key":"e_1_3_2_1_15_1","volume-title":"Solidity documentation. Retrieved","author":"Community Ethereum","year":"2023","unstructured":"Ethereum Community. 2016. Solidity documentation. Retrieved 19 June 2023, Availabe from https:\/\/docs.soliditylang.org\/en\/v0.8.16\/."},{"key":"e_1_3_2_1_16_1","volume-title":"Electronic proceedings of the workshop on dependent types in programming","author":"Hancock Peter","year":"1999","unstructured":"Peter Hancock and Anton Setzer. 1999. The IO monad in dependent type theory. 13 pages. Electronic proceedings of the workshop on dependent types in programming, G\u00f6teborg, 27-28 March 1999."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44622-2_21"},{"key":"e_1_3_2_1_18_1","first-page":"19","volume-title":"Electronic proceedings of the Workshop on subtyping and dependent types in programming, Ponte de Lima, Portugal. 13","author":"Hancock Peter","year":"2000","unstructured":"Peter Hancock and Anton Setzer. 2000. Specifying interactions with dependent types. Electronic proceedings of the Workshop on subtyping and dependent types in programming, Ponte de Lima, Portugal. 13 pp. Retrieved 19 June 2023, Availabe from http:\/\/www-sop.inria.fr\/oasis\/DTP00\/Proceedings\/proceedings.html."},{"key":"e_1_3_2_1_19_1","volume-title":"Dependently typed programming(Dagstuhl Seminar Proceedings, 04381), T.\u00a0Altenkirch, M.\u00a0Hofmann, and J.\u00a0Hughes (Eds.). Internationales Begegnungs- und Forschungszentrum (IBFI)","author":"Hancock Peter","year":"2005","unstructured":"Peter Hancock and Anton Setzer. 2004. Interactive Programs and Weakly Final Coalgebras (Extended Version). In Dependently typed programming(Dagstuhl Seminar Proceedings, 04381), T.\u00a0Altenkirch, M.\u00a0Hofmann, and J.\u00a0Hughes (Eds.). Internationales Begegnungs- und Forschungszentrum (IBFI), Schloss Dagstuhl, Germany, Dagstuhl, Germany, 1 \u2013 30. http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2005\/176\/"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1093\/acprof:oso\/9780198566519.003.0007"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/B978-0-444-51624-4.50004-6"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.comnet.2020.107233"},{"key":"e_1_3_2_1_23_1","volume-title":"Typed Lambda Calculi and Applications","author":"Hurkens Antonius","unstructured":"Antonius J.\u00a0C. Hurkens. 1995. A simplification of Girard\u2019s paradox. In Typed Lambda Calculi and Applications. Springer, Berlin, Heidelberg, 266\u2013278."},{"key":"e_1_3_2_1_24_1","volume-title":"Isabelle documentation. Retrieved","author":"Community Isabelle","year":"2023","unstructured":"Isabelle Community. 2023. Isabelle documentation. Retrieved 19 June 2023, Availabe from https:\/\/isabelle.in.tum.de\/documentation.html."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-015-0378-x"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978309"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-92124-8_23"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71945-1"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-58387-6_28"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/512644.512671"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2022.3143145"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/Cybermatics_2018.2018.00185"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04652-0_5"},{"key":"e_1_3_2_1_35_1","volume-title":"Conference Proceedings of TFP","author":"Setzer Anton","year":"2006","unstructured":"Anton Setzer. 2006. Object-oriented programming in dependent type theory. In Conference Proceedings of TFP 2006. Intellect Books, Bristol, 1 \u2013 16. https:\/\/csetzer.github.io\/index.html"},{"key":"e_1_3_2_1_36_1","volume-title":"Interactive Programs in Agda","author":"Setzer Anton","year":"2023","unstructured":"Anton Setzer. 2009. Interactive Programs in Agda. Swansea University. Retrieved 19 June 2023, Availabe from https:\/\/csetzer.github.io\/slides\/agdaimplementorsmeeting\/agdaImplementorsMeetingGoeteborg2009\/goeteborg2009AgdaIntensiveMeeting.pdf."},{"key":"e_1_3_2_1_37_1","unstructured":"Anton Setzer and Fahad Alhabardi. 2023. A simulator of Solidity-style smart contracts in the theorem prover Agda. Available from https:\/\/github.com\/fahad1985lab\/A_simulator_of_Solidity-style_smart_contracts_in_the_theorem_prover_Agda."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00032"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2841316"},{"key":"e_1_3_2_1_40_1","first-page":"28","article-title":"Smart Contracts: Building Blocks for Digital Markets. EXTROPY","volume":"18","author":"Szabo Nick","year":"1996","unstructured":"Nick Szabo. 1996. Smart Contracts: Building Blocks for Digital Markets. EXTROPY: The Journal of Transhumanist Thought,(16) 18, 2 (1996), 28. Availabe from https:\/\/www.fon.hum.uva.nl\/rob\/Courses\/InformationInSpeech\/CDROM\/Literature\/LOTwinterschool2006\/szabo.best.vwh.net\/smart_contracts_2.html.","journal-title":"The Journal of Transhumanist Thought,(16)"},{"key":"e_1_3_2_1_41_1","volume-title":"Vyper documentation. Retrieved","author":"Team Vyper","year":"2023","unstructured":"Vyper Team. 2017. Vyper documentation. Retrieved 19 June 2023, Availabe from https:\/\/vyper.readthedocs.io\/en\/stable\/."},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1155\/2020\/6191537"}],"event":{"name":"ICBTA 2023: 2023 6th International Conference on Blockchain Technology and Applications","location":"Xi'an China","acronym":"ICBTA 2023"},"container-title":["Proceedings of the 2023 6th International Conference on Blockchain Technology and Applications"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3651655.3651656","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3651655.3651656","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,23]],"date-time":"2025-08-23T18:12:54Z","timestamp":1755972774000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3651655.3651656"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,12,15]]},"references-count":42,"alternative-id":["10.1145\/3651655.3651656","10.1145\/3651655"],"URL":"https:\/\/doi.org\/10.1145\/3651655.3651656","relation":{},"subject":[],"published":{"date-parts":[[2023,12,15]]},"assertion":[{"value":"2024-05-29","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}