{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T01:54:09Z","timestamp":1773194049300,"version":"3.50.1"},"reference-count":75,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2020,9,30]],"date-time":"2020-09-30T00:00:00Z","timestamp":1601424000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100006435","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CNS-1423054, CCF-1814826"],"award-info":[{"award-number":["CNS-1423054, CCF-1814826"]}],"id":[{"id":"10.13039\/100006435","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Ripple, Inc."},{"DOI":"10.13039\/100000005","name":"U.S. Department of Defense","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100000005","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2020,9,30]]},"abstract":"<jats:p>\n            Blockchain platforms are coming into use for processing critical transactions among participants who have not established mutual trust. Many blockchains are programmable, supporting\n            <jats:italic>smart contracts<\/jats:italic>\n            , which maintain persistent state and support transactions that transform the state. Unfortunately, bugs in many smart contracts have been exploited by hackers. Obsidian is a novel programming language with a type system that enables static detection of bugs that are common in smart contracts today. Obsidian is based on a core calculus, Silica, for which we proved type soundness. Obsidian uses\n            <jats:italic>typestate<\/jats:italic>\n            to detect improper state manipulation and uses\n            <jats:italic>linear types<\/jats:italic>\n            to detect abuse of assets. We integrated a permissions system that encodes a notion of\n            <jats:italic>ownership<\/jats:italic>\n            to allow for safe, flexible aliasing. We describe two case studies that evaluate Obsidian\u2019s applicability to the domains of parametric insurance and supply chain management, finding that Obsidian\u2019s type system facilitates reasoning about high-level states and ownership of resources. We compared our Obsidian implementation to a Solidity implementation, observing that the Solidity implementation requires much boilerplate checking and tracking of state, whereas Obsidian does this work statically.\n          <\/jats:p>","DOI":"10.1145\/3417516","type":"journal-article","created":{"date-parts":[[2020,11,26]],"date-time":"2020-11-26T19:51:03Z","timestamp":1606420263000},"page":"1-82","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":24,"title":["Obsidian"],"prefix":"10.1145","volume":"42","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9369-4069","authenticated-orcid":false,"given":"Michael","family":"Coblenz","sequence":"first","affiliation":[{"name":"Carnegie Mellon University, PA, USA"}]},{"given":"Reed","family":"Oei","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, Urbana, IL, USA"}]},{"given":"Tyler","family":"Etzel","sequence":"additional","affiliation":[{"name":"Facebook, CA, USA"}]},{"given":"Paulette","family":"Koronkevich","sequence":"additional","affiliation":[{"name":"University of British Columbia, Vancouver, BC, Canada"}]},{"given":"Miles","family":"Baker","sequence":"additional","affiliation":[{"name":"Amazon, Seattle, WA, USA"}]},{"given":"Yannick","family":"Bloem","sequence":"additional","affiliation":[{"name":"Apple, Inc, Cupertino, CA, USA"}]},{"given":"Brad A.","family":"Myers","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, PA, USA"}]},{"given":"Joshua","family":"Sunshine","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, PA, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0631-5591","authenticated-orcid":false,"given":"Jonathan","family":"Aldrich","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, PA, USA"}]}],"member":"320","published-online":{"date-parts":[[2020,11,25]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","unstructured":"Jonathan Aldrich Joshua Sunshine Darpan Saini and Zachary Sparks. 2009. Typestate-oriented Programming. In Companion of Object Oriented Programming Systems Languages and Applications (OOPSLA\u201909). 1015--1022. DOI:https:\/\/doi.org\/10.1145\/1639950.1640073","DOI":"10.1145\/1639950.1640073"},{"key":"e_1_2_1_2_1","unstructured":"Leonardo Alt and Christian Reitwiessner. 2018. SMT-based verification of solidity smart contracts. In Leveraging Applications of Formal Methods Verification and Validation. Industrial Practice."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03596-9_8"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","unstructured":"Nicola Atzei Massimo Bartoletti and Tiziana Cimoli. 2017. A survey of attacks on ethereum smart contracts SoK. In Principles of Security and Trust (POST\u201917). DOI:https:\/\/doi.org\/10.1007\/978-3-662-54455-6_8","DOI":"10.1007\/978-3-662-54455-6_8"},{"key":"e_1_2_1_5_1","volume-title":"Workshop on Evaluation and Usability of Programming Languages and Tools (PLATEAU\u201917)","author":"Barnaby Celeste","year":"2017","unstructured":"Celeste Barnaby, Michael Coblenz, Tyler Etzel, Eliezer Kanal, Joshua Sunshine, Brad Myers, and Jonathan Aldrich. 2017. A user study to inform the design of the obsidian blockchain DSL. In Workshop on Evaluation and Usability of Programming Languages and Tools (PLATEAU\u201917)."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2993600.2993611"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1370175.1370213"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03013-0_10"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19823-6_4"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44898-5_4"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45337-7_2"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15375-4_16"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","unstructured":"David G. Clarke John M. Potter and James Noble. 1998. Ownership types for flexible alias protection. In Object-oriented Programming Systems Languages and Applications (OOPSLA\u201998). DOI:https:\/\/doi.org\/10.1145\/286936.286947","DOI":"10.1145\/286936.286947"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36946-9"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2688204.2688218"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1184\/R1"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276954.3276965"},{"key":"e_1_2_1_18_1","doi-asserted-by":"crossref","unstructured":"Michael Coblenz Jonathan Aldrich Brad A. Myers and Joshua Sunshine. 2020a. Can advanced type systems be usable? An empirical study of ownership assets and typestate in obsidian. In Object-oriented Programming Systems Languages and Applications (OOPSLA\u201920). Submitted for publication.","DOI":"10.1145\/3428200"},{"key":"e_1_2_1_19_1","volume-title":"Myers","author":"Coblenz Michael","year":"2019","unstructured":"Michael Coblenz, Gauri Kambhatla, Paulette Koronkevich, Jenna L. Wise, Celeste Barnaby, Joshua Sunshine, Jonathan Aldrich, and Brad A. Myers. 2019a. PLIERS: A Process that Integrates User-Centered Methods into Programming Language Design. arxiv:1912.04719. Retrieved from http:\/\/arxiv.org\/abs\/1912.04719."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/WETSEB.2019.00013"},{"key":"e_1_2_1_21_1","volume-title":"Retrieved","author":"Daian Phil","year":"2016","unstructured":"Phil Daian. 2016. Analysis of the DAO exploit. Retrieved August 21, 2018 from http:\/\/hackingdistributed.com\/2016\/06\/18\/analysis-of-the-dao-exploit\/."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24851-4_21"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-53357-4_6"},{"key":"e_1_2_1_24_1","unstructured":"Vincent Dieterich Marko Ivanovic Thomas Meier Sebastian Z\u00e4pfel Manuel Utz and Philipp Sandner. 2017. Retrieved February 18 2020 from https:\/\/medium.com\/@philippsandner\/application-of-blockchain-technology-in-the-manufacturing-industry-d03a8ed3ba5e."},{"key":"e_1_2_1_25_1","volume-title":"Retrieved","author":"Asset Digital","year":"2019","unstructured":"Digital Asset, Inc. 2019. An Introduction to DAML. Retrieved February 18, 2020 from https:\/\/docs.daml.com\/daml\/intro\/0_Intro.html."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/514952.514955"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3173574.3174032"},{"key":"e_1_2_1_28_1","volume-title":"Retrieved","author":"Britannica Encyclop\u00e6dia","year":"2020","unstructured":"Encyclop\u00e6dia Britannica. 2020. Obsidian. Retrieved May 24, 2020 from https:\/\/www.britannica.com\/science\/obsidian."},{"key":"e_1_2_1_29_1","volume-title":"Retrieved","author":"Foundation Ethereum","year":"2020","unstructured":"Ethereum Foundation. 2020c. Common Patterns. Retrieved February 18, 2020 from http:\/\/solidity.readthedocs.io\/en\/develop\/common-patterns.html."},{"key":"e_1_2_1_30_1","volume-title":"Retrieved","author":"Foundation Ethereum","year":"2020","unstructured":"Ethereum Foundation. 2020b. Ethereum Project. Retrieved February 18, 2020 from http:\/\/www.ethereum.org."},{"key":"e_1_2_1_31_1","volume-title":"Retrieved","author":"Foundation Ethereum","year":"2020","unstructured":"Ethereum Foundation. 2020a. Solidity. Retrieved February 18, 2020 from https:\/\/solidity.readthedocs.io\/en\/develop\/."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","unstructured":"Manuel Fahndrich and Robert DeLine. 2002. Adoption and focus: Practical linear types for imperative programming. In Programming Language Design and Implementation (PLDI\u201902). 12. DOI:https:\/\/doi.org\/10.1145\/512529.512532","DOI":"10.1145\/512529.512532"},{"key":"e_1_2_1_33_1","volume-title":"2019 IEEE\/ACM 2nd International Workshop on Emerging Trends in Software Engineering for Blockchain (WETSEB).","author":"Feist J.","unstructured":"J. Feist, G. Grieco, and A. Groce. 2019. Slither: A static analysis framework for smart contracts. In 2019 IEEE\/ACM 2nd International Workshop on Emerging Trends in Software Engineering for Blockchain (WETSEB)."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2629609"},{"key":"e_1_2_1_35_1","volume-title":"Retrieved","author":"Google Inc.","year":"2019","unstructured":"Google Inc. 2019. Protocol Buffers. Retrieved February 18, 2020 from https:\/\/developers.google.com\/protocol-buffers\/."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2398857.2384619"},{"key":"e_1_2_1_37_1","unstructured":"Luke Graham. 2017. $32 million worth of digital currency ether stolen by hackers. Retrieved November 2 2017 from https:\/\/www.cnbc.com\/2017\/07\/20\/32-million-worth-of-digital-currency-ether-stolen-by-hackers.html."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3416262"},{"key":"e_1_2_1_39_1","volume-title":"Retrieved","author":"Review Harvard Business","year":"2017","unstructured":"Harvard Business Review. 2017. The Potential for Blockchain to Transform Electronic Health Records. Retrieved February 18, 2020 from https:\/\/hbr.org\/2017\/03\/the-potential-for-blockchain-to-transform-electronic-health-records."},{"key":"e_1_2_1_40_1","unstructured":"Dominik Harz and William Knottenbelt. 2018. Towards Safer Smart Contracts: A Survey of Languages and Verification Methods. arxiv:1809.09805. Retrieved from http:\/\/arxiv.org\/abs\/1809.09805."},{"key":"e_1_2_1_41_1","volume-title":"International Conference on Service-Oriented Computing (ICSOC\u201916)","author":"Hull Richard","unstructured":"Richard Hull, Vishal S. Batra, Yi-Min Chen, Alin Deutsch, Fenno F. Terry Heath III, and Victor Vianu. 2016. Towards a shared ledger business collaboration language based on data-aware processes. In International Conference on Service-Oriented Computing (ICSOC\u201916)."},{"key":"e_1_2_1_42_1","volume-title":"Retrieved","author":"IBM.","year":"2019","unstructured":"IBM. 2019. Blockchain for supply chain. Retrieved March 31, 2019 from https:\/\/www.ibm.com\/blockchain\/supply-chain\/."},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/503502.503505"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2018.23082"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-30942-8_35"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/319566.319567"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","unstructured":"Loi Luu Duc-Hiep Chu Hrishi Olickel Prateek Saxena and Aquinas Hobor. 2016. Making smart contracts smarter. In Computer and Communications Security (CCS\u201916). DOI:https:\/\/doi.org\/10.1145\/2976749.2978309","DOI":"10.1145\/2976749.2978309"},{"key":"e_1_2_1_48_1","unstructured":"Robert C. Martin Jan M. Rabaey Anantha P. Chandrakasan and Borivoje Nikolic. 2003. Agile Software Development: Principles Patterns and Practices. Pearson Education. 95022672"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0054099"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2016.200"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","unstructured":"Karl Naden Robert Bocchino Jonathan Aldrich and Kevin Bierhoff. 2012. A type system for borrowing permissions. In Principles of Programming Languages (POPL\u201912). DOI:https:\/\/doi.org\/10.1145\/2103621.2103722","DOI":"10.1145\/2103621.2103722"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/97243.97281"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1109\/HCC.2002.1046372"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/345099.345100"},{"key":"e_1_2_1_55_1","volume-title":"Retrieved","author":"Research Mozilla","year":"2015","unstructured":"Mozilla Research. 2015. The Rust Programming Language. Retrieved February 18, 2020 from https:\/\/www.rust-lang.org."},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2010.03.012"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/141471.141563"},{"key":"e_1_2_1_58_1","volume-title":"Retrieved","author":"Schrans Franklin","year":"2019","unstructured":"Franklin Schrans and Susan Eisenbach. 2019. Introduce the Asset trait. Retrieved February 18, 2020 from https:\/\/github.com\/flintlang\/flint\/blob\/master\/proposals\/0001-asset-trait.md."},{"key":"e_1_2_1_59_1","unstructured":"Franklin Schrans Daniel Hails Alexander Harkness Sophia Drossopoulou and Susan Eisenbach. 2019. Flint for safer smart contracts. arxiv:1904.06534. Retrieved from https:\/\/arxiv.org\/abs\/1904.06534."},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","unstructured":"Ilya Sergey Vaivaswatha Nagaraj Jacob Johannsen Amrit Kumar Anton Trunov and Ken Chan Guan Hao. 2019. Safer smart contract programming with Scilla. In Object-oriented Programming Systems Languages and Applications (OOPSLA\u201919). DOI:https:\/\/doi.org\/10.1145\/3360611","DOI":"10.1145\/3360611"},{"key":"e_1_2_1_61_1","volume-title":"Retrieved","author":"Sirer Emin G\u00fcn","year":"2016","unstructured":"Emin G\u00fcn Sirer. 2016. Thoughts on The DAO Hack. Retrieved February 18, 2020 from http:\/\/hackingdistributed.com\/2016\/06\/17\/thoughts-on-the-dao-hack\/."},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/2661136.2661156"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/2534973"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1986.6312929"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2007.92"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44202-9_7"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","unstructured":"Joshua Sunshine Karl Naden Sven Stork Jonathan Aldrich and \u00c9ric Tanter. 2011. First-class state change in Plaid. In Object Oriented Programming Systems Languages and Applications (OOPSLA\u201911). DOI:https:\/\/doi.org\/10.1145\/2076021.2048122","DOI":"10.1145\/2076021.2048122"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.5210\/fm.v2i9.548"},{"key":"e_1_2_1_69_1","volume-title":"Retrieved","author":"Foundation The Linux","year":"2020","unstructured":"The Linux Foundation. 2020. Hyperledger Fabric. Retrieved February 18, 2020 from https:\/\/www.hyperledger.org\/projects\/fabric."},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926436"},{"key":"e_1_2_1_71_1","volume-title":"Retrieved","author":"Vogelsteller Fabian","year":"2015","unstructured":"Fabian Vogelsteller and Vitalik Buterin. 2015. EIP 20: ERC-20 Token Standard. Retrieved February 18, 2020 from https:\/\/eips.ethereum.org\/EIPS\/eip-20."},{"key":"e_1_2_1_72_1","first-page":"347","article-title":"Linear types can change the world","volume":"2","author":"Wadler Philip","year":"1990","unstructured":"Philip Wadler. 1990. Linear types can change the world. In Programming Concepts and Methods, Vol. 2. 347--359.","journal-title":"Programming Concepts and Methods"},{"key":"e_1_2_1_73_1","doi-asserted-by":"crossref","unstructured":"Max Willsey Rokhini Prabhu and Frank Pfenning. 2017. Design and Implementation of Concurrent C0. arxiv:cs.PL\/1701.04929. Retrieved from https:\/\/arxiv.org\/abs\/1701.04929.","DOI":"10.4204\/EPTCS.238.8"},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSA.2017.33"},{"key":"e_1_2_1_75_1","doi-asserted-by":"crossref","unstructured":"Jakub Zakrzewski. 2018. Towards verification of ethereum smart contracts: A formalization of core of solidity. In Verified Software. Theories Tools and Experiments.","DOI":"10.1007\/978-3-030-03592-1_13"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3417516","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3417516","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3417516","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:01:14Z","timestamp":1750197674000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3417516"}},"subtitle":["Typestate and Assets for Safer Blockchain Programming"],"short-title":[],"issued":{"date-parts":[[2020,9,30]]},"references-count":75,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2020,9,30]]}},"alternative-id":["10.1145\/3417516"],"URL":"https:\/\/doi.org\/10.1145\/3417516","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,9,30]]},"assertion":[{"value":"2019-08-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-08-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-11-25","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}