{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T18:40:24Z","timestamp":1742928024815,"version":"3.40.3"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031770180"},{"type":"electronic","value":"9783031770197"}],"license":[{"start":{"date-parts":[[2024,11,22]],"date-time":"2024-11-22T00:00:00Z","timestamp":1732233600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,11,22]],"date-time":"2024-11-22T00:00:00Z","timestamp":1732233600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-77019-7_18","type":"book-chapter","created":{"date-parts":[[2024,11,21]],"date-time":"2024-11-21T20:48:02Z","timestamp":1732222082000},"page":"313-330","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Type Safety for\u00a0Isabelle\/Solidity"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7242-5890","authenticated-orcid":false,"given":"Billy","family":"Thornton","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2859-7673","authenticated-orcid":false,"given":"Diego","family":"Marmsoler","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,11,22]]},"reference":[{"key":"18_CR1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-49812-6","volume-title":"Deductive Software Verification-the Key Book","author":"W Ahrendt","year":"2016","unstructured":"Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Schmitt, P.H., Ulbrich, M.: Deductive Software Verification-the Key Book, vol. 10001. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-49812-6"},{"key":"18_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1007\/978-3-030-61467-6_2","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Applications","author":"W Ahrendt","year":"2020","unstructured":"Ahrendt, W., Bubel, R.: Functional verification of smart contracts via strong data integrity. In: Margaria, T., Steffen, B. (eds.) ISoLA 2020. LNCS, vol. 12478, pp. 9\u201324. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-61467-6_2"},{"key":"18_CR3","doi-asserted-by":"publisher","first-page":"101227","DOI":"10.1016\/j.pmcj.2020.101227","volume":"67","author":"M Almakhour","year":"2020","unstructured":"Almakhour, M., Sliman, L., Samhat, A.E., Mellouk, A.: Verification of smart contracts: a survey. Pervasive Mob. Comput. 67, 101227 (2020). https:\/\/doi.org\/10.1016\/j.pmcj.2020.101227","journal-title":"Pervasive Mob. Comput."},{"key":"18_CR4","unstructured":"Authors, S.: Solidity developer survey 2023 results (2024). https:\/\/soliditylang.org\/blog\/2024\/04\/03\/solidity-developer-survey-2023-results\/"},{"key":"18_CR5","doi-asserted-by":"publisher","unstructured":"Azaria, A., Ekblaw, A., Vieira, T., Lippman, A.: MedRec: using blockchain for medical data access and permission management. In: 2016 2nd International Conference on Open and Big Data (OBD), pp. 25\u201330 (2016). https:\/\/doi.org\/10.1109\/OBD.2016.11","DOI":"10.1109\/OBD.2016.11"},{"key":"18_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-030-31500-9_15","volume-title":"Data Privacy Management, Cryptocurrencies and Blockchain Technology","author":"M Bartoletti","year":"2019","unstructured":"Bartoletti, M., Galletta, L., Murgia, M.: A minimal core calculus for solidity contracts. In: P\u00e9rez-Sol\u00e0, C., Navarro-Arribas, G., Biryukov, A., Garcia-Alfaro, J. (eds.) DPM\/CBT -2019. LNCS, vol. 11737, pp. 233\u2013243. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-31500-9_15"},{"key":"18_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/3-540-48256-3_3","volume-title":"Theorem Proving in Higher Order Logics","author":"S Berghofer","year":"1999","unstructured":"Berghofer, S., Wenzel, M.: Inductive datatypes in HOL \u2014 lessons learned in formal-logic engineering. In: Bertot, Y., Dowek, G., Th\u00e9ry, L., Hirschowitz, A., Paulin, C. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 19\u201336. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48256-3_3"},{"key":"18_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/978-3-642-38348-9_19","volume-title":"Advances in Cryptology \u2013 EUROCRYPT 2013","author":"G Bertoni","year":"2013","unstructured":"Bertoni, G., Daemen, J., Peeters, M., Van Assche, G.: Keccak. In: Johansson, T., Nguyen, P.Q. (eds.) EUROCRYPT 2013. LNCS, vol. 7881, pp. 313\u2013314. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38348-9_19"},{"key":"18_CR9","doi-asserted-by":"publisher","unstructured":"Bhargavan, K., et al.: Formal verification of smart contracts: Short paper. In: Programming Languages and Analysis for Security, pp. 91\u201396. PLAS, ACM (2016).https:\/\/doi.org\/10.1145\/2993600.2993611","DOI":"10.1145\/2993600.2993611"},{"key":"18_CR10","unstructured":"Chavez-Dreyfuss, G.: Sweden tests blockchain technology for land registry. https:\/\/www.reuters.com\/article\/us-sweden-blockchain-idUSKCN0Z22KV. Accessed 18 Apr 2023"},{"key":"18_CR11","unstructured":"Clegg, P., Jevans, D.: Cryptocurrency crime and anti-money laundering report. Technical report, CipherTrace (2021)"},{"key":"18_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"138","DOI":"10.1007\/978-3-030-43725-1_11","volume-title":"Financial Cryptography and Data Security","author":"S Crafa","year":"2020","unstructured":"Crafa, S., Di Pirro, M., Zucca, E.: Is solidity solid enough? In: Bracciali, A., Clark, J., Pintore, F., R\u00f8nne, P.B., Sala, M. (eds.) FC 2019. LNCS, vol. 11599, pp. 138\u2013153. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-43725-1_11"},{"key":"18_CR13","unstructured":"Crosara, M., Centurino, G., Arceri, V.: Towards an operational semantics for solidity. In: van Rooyen, J., Buro, S., Campion, M., Pasqua, M. (eds.) VALID, pp.\u00a01\u20136. IARIA (2019)"},{"key":"18_CR14","unstructured":"Ethereum: Solidity. https:\/\/docs.soliditylang.org\/. Accessed 04 May 2023"},{"key":"18_CR15","doi-asserted-by":"publisher","unstructured":"Jiao, J., Kan, S., Lin, S.W., Sanan, D., Liu, Y., Sun, J.: Semantic understanding of smart contracts: executable operational semantics of Solidity. In: SP, pp. 1695\u20131712. IEEE (2020). https:\/\/doi.org\/10.1109\/SP40000.2020.00066","DOI":"10.1109\/SP40000.2020.00066"},{"key":"18_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/978-3-030-45234-6_4","volume-title":"Fundamental Approaches to Software Engineering","author":"J Jiao","year":"2020","unstructured":"Jiao, J., Lin, S.-W., Sun, J.: A generalized formal semantic framework for smart contracts. In: FASE 2020. LNCS, vol. 12076, pp. 75\u201396. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45234-6_4"},{"key":"18_CR17","unstructured":"Kelly, J.: Banks adopting blockchain \u2018dramatically faster\u2019 than expected: IBM (2016). https:\/\/www.reuters.com\/article\/us-tech-blockchain-ibm-idUSKCN11Y28D. Accessed 04 May 2023"},{"key":"18_CR18","unstructured":"Llama, D.: TVL breakdown by smart contract language (2024). https:\/\/defillama.com\/languages"},{"key":"18_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1007\/978-3-030-92124-8_23","volume-title":"Software Engineering and Formal Methods","author":"D Marmsoler","year":"2021","unstructured":"Marmsoler, D., Brucker, A.D.: A denotational semantics of\u00a0solidity in\u00a0Isabelle\/HOL. In: Calinescu, R., P\u0103s\u0103reanu, C.S. (eds.) SEFM 2021. LNCS, vol. 13085, pp. 403\u2013422. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-92124-8_23"},{"key":"18_CR20","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1007\/978-3-031-09827-7_7","volume-title":"TAP 2022","author":"D Marmsoler","year":"2022","unstructured":"Marmsoler, D., Brucker, A.D.: Conformance testing of formal semantics using grammar-based fuzzing. In: Kov\u00e1cs, L., Meinke, K. (eds.) TAP 2022. LNCS, vol. 13361, pp. 106\u2013125. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-09827-7_7"},{"key":"18_CR21","unstructured":"Marmsoler, D., Brucker, A.D.: Isabelle\/solidity:a deep embedding of solidity in isabelle\/hol. Archive of Formal Proofs (2022). https:\/\/isa-afp.org\/entries\/Solidity.html, Formal proof development"},{"key":"18_CR22","doi-asserted-by":"publisher","unstructured":"Mendling, J., et al.: Blockchains for business process management - challenges and opportunities. ACM Trans. Manage. Inf. Syst. 9(1) (2018).https:\/\/doi.org\/10.1145\/3183367","DOI":"10.1145\/3183367"},{"key":"18_CR23","doi-asserted-by":"publisher","unstructured":"Nakamoto, S.: Bitcoin: a peer-to-peer electronic cash system (2008). https:\/\/doi.org\/10.2139\/ssrn.3440802","DOI":"10.2139\/ssrn.3440802"},{"key":"18_CR24","doi-asserted-by":"publisher","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: a proof assistant for higher-order logic (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9","DOI":"10.1007\/3-540-45949-9"},{"key":"18_CR25","doi-asserted-by":"publisher","unstructured":"Nipkow, T., Klein, G.: Concrete Semantics: With Isabelle\/HOL. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10542-0","DOI":"10.1007\/978-3-319-10542-0"},{"key":"18_CR26","doi-asserted-by":"publisher","unstructured":"Tolmach, P., Li, Y., Lin, S.W., Liu, Y., Li, Z.: A survey of smart contract formal specification and verification. ACM Comput. Surv. 54(7) (2021). https:\/\/doi.org\/10.1145\/3464421","DOI":"10.1145\/3464421"},{"key":"18_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/3-540-48737-9_4","volume-title":"Formal Syntax and Semantics of Java","author":"D von Oheimb","year":"1999","unstructured":"von Oheimb, D., Nipkow, T.: Machine-checking the java specification: proving type-safety. In: Alves-Foss, J. (ed.) Formal Syntax and Semantics of Java. LNCS, vol. 1523, pp. 119\u2013156. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48737-9_4"},{"key":"18_CR28","doi-asserted-by":"publisher","unstructured":"Wasserrab, D., Nipkow, T., Snelting, G., Tip, F.: An operational semantics and type safety proof for multiple inheritance in c++. In: Proceedings of the 21st Annual ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages, and Applications, pp. 345\u2013362 (2006).https:\/\/doi.org\/10.1145\/1167515.1167503","DOI":"10.1145\/1167515.1167503"},{"key":"18_CR29","unstructured":"YCharts.com: Ethereum transactions per day. https:\/\/ycharts.com\/indicators\/ethereum_transactions_per_day. Accessed 04 May 2024"},{"key":"18_CR30","unstructured":"Yurcan, B.: How blockchain fits into the future of digital identity (2016). https:\/\/fintechranking.com\/2016\/04\/10\/how-blockchain-fits-into-the-future-of-digital-identity\/"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2024"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-77019-7_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,21]],"date-time":"2024-11-21T21:30:24Z","timestamp":1732224624000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-77019-7_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,22]]},"ISBN":["9783031770180","9783031770197"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-77019-7_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,11,22]]},"assertion":[{"value":"22 November 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICTAC","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Colloquium on Theoretical Aspects of Computing","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Bangkok","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Thailand","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 November 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 November 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ictac2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ictac2024.cs.ait.ac.th\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}