{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,2]],"date-time":"2026-10-02T08:05:05Z","timestamp":1790928305835,"version":"4.1.0"},"reference-count":95,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2019,10,10]],"date-time":"2019-10-10T00:00:00Z","timestamp":1570665600000},"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":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,10,10]]},"abstract":"<jats:p>The rise of programmable open distributed consensus platforms based on the blockchain technology has aroused a lot of interest in replicated stateful computations, aka smart contracts. As blockchains are used predominantly in financial applications, smart contracts frequently manage millions of dollars worth of virtual coins. Since smart contracts cannot be updated once deployed, the ability to reason about their correctness becomes a critical task. Yet, the de facto implementation standard, pioneered by the Ethereum platform, dictates smart contracts to be deployed in a low-level language, which renders independent audit and formal verification of deployed code infeasible in practice.<\/jats:p>\n          <jats:p>We report an ongoing experiment held with an industrial blockchain vendor on designing, evaluating, and deploying Scilla, a new programming language for safe smart contracts. Scilla is positioned as an intermediate-level language, suitable to serve as a compilation target and also as an independent programming framework. Taking System F as a foundational calculus, Scilla offers strong safety guarantees by means of type soundness. It provides a clean separation between pure computational, state-manipulating, and communication aspects of smart contracts, avoiding many known pitfalls due to execution in a byzantine environment. We describe the motivation, design principles, and semantics of Scilla, and we report on Scilla use cases provided by the developer community. Finally, we present a framework for lightweight verification of Scilla programs, and showcase it with two domain-specific analyses on a suite of real-world use cases.<\/jats:p>","DOI":"10.1145\/3360611","type":"journal-article","created":{"date-parts":[[2019,10,11]],"date-time":"2019-10-11T14:53:33Z","timestamp":1570805613000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":80,"title":["Safer smart contract programming with Scilla"],"prefix":"10.1145","volume":"3","author":[{"given":"Ilya","family":"Sergey","sequence":"first","affiliation":[{"name":"Yale-NUS College, Singapore \/ National University of Singapore, Singapore"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Vaivaswatha","family":"Nagaraj","sequence":"additional","affiliation":[{"name":"Zilliqa Research, India"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jacob","family":"Johannsen","sequence":"additional","affiliation":[{"name":"Zilliqa Research, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Amrit","family":"Kumar","sequence":"additional","affiliation":[{"name":"Zilliqa Research, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Anton","family":"Trunov","sequence":"additional","affiliation":[{"name":"Zilliqa Research, Russia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ken Chan Guan","family":"Hao","sequence":"additional","affiliation":[{"name":"Zilliqa Research, Malaysia"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,10,10]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"SAS (LNCS)","author":"Albert Elvira","unstructured":"Elvira Albert , Puri Arenas , Samir Genaim , and Germ\u00e1n Puebla . 2008. Automatic Inference of Upper Bounds for Recurrence Relations in Cost Analysis . In SAS (LNCS) , Vol. 5079 . Springer , 221\u2013237. Elvira Albert, Puri Arenas, Samir Genaim, and Germ\u00e1n Puebla. 2008. Automatic Inference of Upper Bounds for Recurrence Relations in Cost Analysis. In SAS (LNCS), Vol. 5079. Springer, 221\u2013237."},{"key":"e_1_2_2_2_1","unstructured":"Gabriel Alfour. 2019. Introducing LIGO: a new smart contract language for Tezos. https:\/\/medium.com\/tezos\/introducingligo-a-new-smart-contract-language-for-tezos-233fa17f21c7 .  Gabriel Alfour. 2019. Introducing LIGO: a new smart contract language for Tezos. https:\/\/medium.com\/tezos\/introducingligo-a-new-smart-contract-language-for-tezos-233fa17f21c7 ."},{"key":"e_1_2_2_3_1","unstructured":"JD Alois. 2017. Ethereum Parity Hack May Impact ETH 500 000 or $146 Million. https:\/\/www.crowdfundinsider.com\/2017\/ 11\/124200-ethereum-parity-hack-may-impact-eth-500000-146-million\/ .  JD Alois. 2017. Ethereum Parity Hack May Impact ETH 500 000 or $146 Million. https:\/\/www.crowdfundinsider.com\/2017\/ 11\/124200-ethereum-parity-hack-may-impact-eth-500000-146-million\/ ."},{"key":"e_1_2_2_4_1","volume-title":"ISoLA (LNCS)","author":"Alt Leonardo","unstructured":"Leonardo Alt and Christian Reitwie\u00dfner . 2018. SMT-Based Verification of Solidity Smart Contracts . In ISoLA (LNCS) , Vol. 11247 . Springer , 376\u2013388. Leonardo Alt and Christian Reitwie\u00dfner. 2018. SMT-Based Verification of Solidity Smart Contracts. In ISoLA (LNCS), Vol. 11247. Springer, 376\u2013388."},{"key":"e_1_2_2_5_1","doi-asserted-by":"crossref","unstructured":"Sidney Amani Myriam B\u00e9gel Maksym Bortin and Mark Staples. 2018. Towards verifying Ethereum smart contract bytecode in Isabelle\/HOL. In CPP. ACM 66\u201377.  Sidney Amani Myriam B\u00e9gel Maksym Bortin and Mark Staples. 2018. Towards verifying Ethereum smart contract bytecode in Isabelle\/HOL. In CPP. ACM 66\u201377.","DOI":"10.1145\/3176245.3167084"},{"key":"e_1_2_2_6_1","doi-asserted-by":"crossref","unstructured":"Nada Amin and Tiark Rompf. 2017. Type soundness proofs with definitional interpreters. In POPL. ACM 666\u2013679.  Nada Amin and Tiark Rompf. 2017. Type soundness proofs with definitional interpreters. In POPL. ACM 666\u2013679.","DOI":"10.1145\/3093333.3009866"},{"key":"e_1_2_2_7_1","volume-title":"POST (LNCS)","author":"Atzei Nicola","unstructured":"Nicola Atzei , Massimo Bartoletti , and Tiziana Cimoli . 2017. A Survey of Attacks on Ethereum Smart Contracts (SoK) . In POST (LNCS) , Vol. 10204 . Springer , 164\u2013186. Nicola Atzei, Massimo Bartoletti, and Tiziana Cimoli. 2017. A Survey of Attacks on Ethereum Smart Contracts (SoK). In POST (LNCS), Vol. 10204. Springer, 164\u2013186."},{"key":"e_1_2_2_8_1","volume-title":"Consensus in the Age of Blockchains. CoRR abs\/1711.03936","author":"Bano Shehar","year":"2017","unstructured":"Shehar Bano , Alberto Sonnino , Mustafa Al-Bassam , Sarah Azouvi , Patrick McCorry , Sarah Meiklejohn , and George Danezis . 2017. Consensus in the Age of Blockchains. CoRR abs\/1711.03936 ( 2017 ). Shehar Bano, Alberto Sonnino, Mustafa Al-Bassam, Sarah Azouvi, Patrick McCorry, Sarah Meiklejohn, and George Danezis. 2017. Consensus in the Age of Blockchains. CoRR abs\/1711.03936 (2017)."},{"key":"e_1_2_2_9_1","volume-title":"TACAS (LNCS)","author":"Bansal Kshitij","unstructured":"Kshitij Bansal , Eric Koskinen , and Omer Tripp . 2018. Automatic Generation of Precise and Useful Commutativity Conditions . In TACAS (LNCS) , Vol. 10805 . Springer , 115\u2013132. Kshitij Bansal, Eric Koskinen, and Omer Tripp. 2018. Automatic Generation of Precise and Useful Commutativity Conditions. In TACAS (LNCS), Vol. 10805. Springer, 115\u2013132."},{"key":"e_1_2_2_10_1","doi-asserted-by":"crossref","unstructured":"Karthikeyan Bhargavan Antoine Delignat-Lavaud C\u00e9dric Fournet Anitha Gollamudi Georges Gonthier Nadim Kobeissi Natalia Kulatova Aseem Rastogi Thomas Sibut-Pinote Nikhil Swamy and Santiago Zanella-B\u00e9guelin. 2016. Formal Verification of Smart Contracts: Short Paper. In PLAS. ACM 91\u201396.  Karthikeyan Bhargavan Antoine Delignat-Lavaud C\u00e9dric Fournet Anitha Gollamudi Georges Gonthier Nadim Kobeissi Natalia Kulatova Aseem Rastogi Thomas Sibut-Pinote Nikhil Swamy and Santiago Zanella-B\u00e9guelin. 2016. Formal Verification of Smart Contracts: Short Paper. In PLAS. ACM 91\u201396.","DOI":"10.1145\/2993600.2993611"},{"key":"e_1_2_2_11_1","volume-title":"https:\/\/en.bitcoin.it\/wiki\/Script , accessed on","author":"Wiki Bitcoin","year":"2019","unstructured":"Bitcoin Wiki . 2017. Bitcoin Script . https:\/\/en.bitcoin.it\/wiki\/Script , accessed on Apr 5, 2019 . Bitcoin Wiki. 2017. Bitcoin Script. https:\/\/en.bitcoin.it\/wiki\/Script , accessed on Apr 5, 2019."},{"key":"e_1_2_2_12_1","volume-title":"Move: A Language With Programmable Resources. https:\/\/developers.libra.org\/docs\/assets\/papers\/libra-move-a-language-with-programmable-resources.pdf .","author":"Blackshear Sam","year":"2019","unstructured":"Sam Blackshear , Evan Cheng , David L. Dill , Victor Gao , Ben Maurer , Todd Nowacki , Alistair Pott , Shaz Qadeer , Rain, Dario Russi , Stephane Sezer , Tim Zakian , and Runtian Zhou . 2019 . Move: A Language With Programmable Resources. https:\/\/developers.libra.org\/docs\/assets\/papers\/libra-move-a-language-with-programmable-resources.pdf . Sam Blackshear, Evan Cheng, David L. Dill, Victor Gao, Ben Maurer, Todd Nowacki, Alistair Pott, Shaz Qadeer, Rain, Dario Russi, Stephane Sezer, Tim Zakian, and Runtian Zhou. 2019. Move: A Language With Programmable Resources. https:\/\/developers.libra.org\/docs\/assets\/papers\/libra-move-a-language-with-programmable-resources.pdf ."},{"key":"e_1_2_2_13_1","volume-title":"sCompile: Critical Path Identification and Analysis for Smart Contracts. CoRR abs\/1808.00624","author":"Chang Jialiang","year":"2018","unstructured":"Jialiang Chang , Bo Gao , Hao Xiao , Jun Sun , and Zijiang Yang . 2018. sCompile: Critical Path Identification and Analysis for Smart Contracts. CoRR abs\/1808.00624 ( 2018 ). Jialiang Chang, Bo Gao, Hao Xiao, Jun Sun, and Zijiang Yang. 2018. sCompile: Critical Path Identification and Analysis for Smart Contracts. CoRR abs\/1808.00624 (2018)."},{"key":"e_1_2_2_14_1","volume-title":"ESOP (LNCS)","author":"Chargu\u00e9raud Arthur","unstructured":"Arthur Chargu\u00e9raud . 2013. Pretty-Big-Step Semantics . In ESOP (LNCS) , Vol. 7792 . Springer , 41\u201360. Arthur Chargu\u00e9raud. 2013. Pretty-Big-Step Semantics. In ESOP (LNCS), Vol. 7792. Springer, 41\u201360."},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/SANER.2017.7884650"},{"key":"e_1_2_2_16_1","volume-title":"Obsidian: A Safer Blockchain Programming Language. In ICSE (Companion)","author":"Coblenz Michael","year":"2017","unstructured":"Michael Coblenz . 2017 . Obsidian: A Safer Blockchain Programming Language. In ICSE (Companion) . IEEE Press , 97\u201399. Michael Coblenz. 2017. Obsidian: A Safer Blockchain Programming Language. In ICSE (Companion). IEEE Press, 97\u201399."},{"key":"e_1_2_2_17_1","unstructured":"Coq Development Team. 2019. The Coq Proof Assistant Reference Manual - Version 8.9. http:\/\/coq.inria.fr .  Coq Development Team. 2019. The Coq Proof Assistant Reference Manual - Version 8.9. http:\/\/coq.inria.fr ."},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796819000042"},{"key":"e_1_2_2_20_1","doi-asserted-by":"crossref","unstructured":"Olivier Danvy and Andrzej Filinski. 1990. Abstracting Control. In LISP and Functional Programming. 151\u2013160.  Olivier Danvy and Andrzej Filinski. 1990. Abstracting Control. In LISP and Functional Programming. 151\u2013160.","DOI":"10.1145\/91556.91622"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500001535"},{"key":"e_1_2_2_22_1","doi-asserted-by":"crossref","unstructured":"Olivier Danvy and J. Michael Spivey. 2007. On Barron and Strachey\u2019s cartesian product function. In ICFP. ACM 41\u201346.  Olivier Danvy and J. Michael Spivey. 2007. On Barron and Strachey\u2019s cartesian product function. In ICFP. ACM 41\u201346.","DOI":"10.1145\/1291220.1291161"},{"key":"e_1_2_2_23_1","volume-title":"The DAO Attacked: Code Issue Leads to $60 Million Ether Theft. https:\/\/www.coindesk.com\/daoattacked-code-issue-leads-60-million-ether-theft\/ , accessed on","author":"del Castillo Michael","year":"2017","unstructured":"Michael del Castillo . 2016. The DAO Attacked: Code Issue Leads to $60 Million Ether Theft. https:\/\/www.coindesk.com\/daoattacked-code-issue-leads-60-million-ether-theft\/ , accessed on Dec 2, 2017 . Michael del Castillo. 2016. The DAO Attacked: Code Issue Leads to $60 Million Ether Theft. https:\/\/www.coindesk.com\/daoattacked-code-issue-leads-60-million-ether-theft\/ , accessed on Dec 2, 2017."},{"key":"e_1_2_2_24_1","volume-title":"Schiller","author":"Dietl Werner","year":"2011","unstructured":"Werner Dietl , Stephanie Dietzel , Michael D. Ernst , Kivan\u00e7 Muslu , and Todd W . Schiller . 2011 . Building and using pluggable type-checkers. In ICSE. ACM , 681\u2013690. Werner Dietl, Stephanie Dietzel, Michael D. Ernst, Kivan\u00e7 Muslu, and Todd W. Schiller. 2011. Building and using pluggable type-checkers. In ICSE. ACM, 681\u2013690."},{"key":"e_1_2_2_25_1","unstructured":"Ethereum Foundation. 2018a. Decentralized Autonomous Organization. https:\/\/www.ethereum.org\/dao .  Ethereum Foundation. 2018a. Decentralized Autonomous Organization. https:\/\/www.ethereum.org\/dao ."},{"key":"e_1_2_2_26_1","unstructured":"Ethereum Foundation. 2018b. ERC20 Token Standard. https:\/\/theethereum.wiki\/w\/index.php\/ERC20_Token_Standard .  Ethereum Foundation. 2018b. ERC20 Token Standard. https:\/\/theethereum.wiki\/w\/index.php\/ERC20_Token_Standard ."},{"key":"e_1_2_2_27_1","volume-title":"List of Known Solidity Bugs. https:\/\/solidity.readthedocs.io\/en\/v0.5.7\/bugs.html , accessed on","author":"Foundation Ethereum","year":"2019","unstructured":"Ethereum Foundation . 2018c. List of Known Solidity Bugs. https:\/\/solidity.readthedocs.io\/en\/v0.5.7\/bugs.html , accessed on Apr 5, 2019 . Ethereum Foundation. 2018c. List of Known Solidity Bugs. https:\/\/solidity.readthedocs.io\/en\/v0.5.7\/bugs.html , accessed on Apr 5, 2019."},{"key":"e_1_2_2_28_1","unstructured":"Ethereum Foundation. 2018d. Solidity Documentation. http:\/\/solidity.readthedocs.io .  Ethereum Foundation. 2018d. Solidity Documentation. http:\/\/solidity.readthedocs.io ."},{"key":"e_1_2_2_29_1","unstructured":"Ethereum Foundation. 2018e. Vyper. https:\/\/vyper.readthedocs.io .  Ethereum Foundation. 2018e. Vyper. https:\/\/vyper.readthedocs.io ."},{"key":"e_1_2_2_30_1","unstructured":"Ethereum Foundation. 2018f. Yul. https:\/\/solidity.readthedocs.io\/en\/latest\/yul.html .  Ethereum Foundation. 2018f. Yul. https:\/\/solidity.readthedocs.io\/en\/latest\/yul.html ."},{"key":"e_1_2_2_31_1","volume-title":"Representing Monads","author":"Filinski Andrzej","unstructured":"Andrzej Filinski . 1994. Representing Monads . In POPL. ACM Press , 446\u2013457. Andrzej Filinski. 1994. Representing Monads. In POPL. ACM Press, 446\u2013457."},{"key":"e_1_2_2_32_1","doi-asserted-by":"crossref","unstructured":"Cormac Flanagan Amr Sabry Bruce F. Duba and Matthias Felleisen. 1993. The Essence of Compiling with Continuations. In PLDI. ACM 237\u2013247.  Cormac Flanagan Amr Sabry Bruce F. Duba and Matthias Felleisen. 1993. The Essence of Compiling with Continuations. In PLDI. ACM 237\u2013247.","DOI":"10.1145\/173262.155113"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276486"},{"key":"e_1_2_2_36_1","volume-title":"POST (LNCS)","author":"Grishchenko Ilya","unstructured":"Ilya Grishchenko , Matteo Maffei , and Clara Schneidewind . 2018. A Semantic Framework for the Security Analysis of Ethereum Smart Contracts . In POST (LNCS) , Vol. 10804 . Springer , 243\u2013269. Ilya Grishchenko, Matteo Maffei, and Clara Schneidewind. 2018. A Semantic Framework for the Security Analysis of Ethereum Smart Contracts. In POST (LNCS), Vol. 10804. Springer, 243\u2013269."},{"key":"e_1_2_2_37_1","volume-title":"POPL","author":"Grossman Shelly","year":"2018","unstructured":"Shelly Grossman , Ittai Abraham , Guy Golan-Gueta , Yan Michalevsky , Noam Rinetzky , Mooly Sagiv , and Yoni Zohar . 2018. Online detection of effectively callback free objects with applications to smart contracts. PACMPL 2 , POPL ( 2018 ). Shelly Grossman, Ittai Abraham, Guy Golan-Gueta, Yan Michalevsky, Noam Rinetzky, Mooly Sagiv, and Yoni Zohar. 2018. Online detection of effectively callback free objects with applications to smart contracts. PACMPL 2, POPL (2018)."},{"key":"e_1_2_2_38_1","unstructured":"Emin G\u00fcn Sirer. 2016. Reentrancy Woes in Smart Contracts. http:\/\/hackingdistributed.com\/2016\/07\/13\/reentrancy-woes\/  Emin G\u00fcn Sirer. 2016. Reentrancy Woes in Smart Contracts. http:\/\/hackingdistributed.com\/2016\/07\/13\/reentrancy-woes\/"},{"key":"e_1_2_2_39_1","doi-asserted-by":"crossref","unstructured":"Robert Harper. 2012. Practical Foundations for Programming Languages. Version 1.32.  Robert Harper. 2012. Practical Foundations for Programming Languages. Version 1.32.","DOI":"10.1017\/CBO9781139342131"},{"key":"e_1_2_2_40_1","unstructured":"Yoichi Hirai. 2018. Bamboo. https:\/\/github.com\/pirapira\/bamboo .  Yoichi Hirai. 2018. Bamboo. https:\/\/github.com\/pirapira\/bamboo ."},{"key":"e_1_2_2_41_1","doi-asserted-by":"crossref","unstructured":"Jan Hoffmann Ankush Das and Shu-Chun Weng. 2017. Towards automatic resource bound analysis for OCaml. In POPL. ACM 359\u2013373.  Jan Hoffmann Ankush Das and Shu-Chun Weng. 2017. Towards automatic resource bound analysis for OCaml. In POPL. ACM 359\u2013373.","DOI":"10.1145\/3093333.3009842"},{"key":"e_1_2_2_42_1","volume-title":"Marlowe: A Contract Language For The Financial World. https:\/\/testnet.iohkdev.io\/marlowe\/ .","author":"Foundation IOHK","year":"2019","unstructured":"IOHK Foundation . 2019 a. Marlowe: A Contract Language For The Financial World. https:\/\/testnet.iohkdev.io\/marlowe\/ . IOHK Foundation. 2019a. Marlowe: A Contract Language For The Financial World. https:\/\/testnet.iohkdev.io\/marlowe\/ ."},{"key":"e_1_2_2_43_1","volume-title":"Plutus: A Functional Contract Platform. https:\/\/testnet.iohkdev.io\/plutus\/ .","author":"Foundation IOHK","year":"2019","unstructured":"IOHK Foundation . 2019 b. Plutus: A Functional Contract Platform. https:\/\/testnet.iohkdev.io\/plutus\/ . IOHK Foundation. 2019b. Plutus: A Functional Contract Platform. https:\/\/testnet.iohkdev.io\/plutus\/ ."},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263765"},{"key":"e_1_2_2_45_1","volume-title":"Zeus: Analyzing Safety of Smart Contracts. In NDSS.","author":"Kalra Sukrit","year":"2018","unstructured":"Sukrit Kalra , Seep Goel , Mohan Dhawan , and Subodh Sharma . 2018 . Zeus: Analyzing Safety of Smart Contracts. In NDSS. Sukrit Kalra, Seep Goel, Mohan Dhawan, and Subodh Sharma. 2018. Zeus: Analyzing Safety of Smart Contracts. In NDSS."},{"key":"e_1_2_2_46_1","volume-title":"Relational Parametricity and Units of Measure","author":"Kennedy Andrew","unstructured":"Andrew Kennedy . 1997. Relational Parametricity and Units of Measure . In POPL. ACM Press , 442\u2013455. Andrew Kennedy. 1997. Relational Parametricity and Units of Measure. In POPL. ACM Press, 442\u2013455."},{"key":"e_1_2_2_47_1","volume-title":"Exploiting The Laws of Order in Smart Contracts. CoRR abs\/1810.11605","author":"Kolluri Aashish","year":"2018","unstructured":"Aashish Kolluri , Ivica Nikoli\u0107 , Ilya Sergey , Aquinas Hobor , and Prateek Saxena . 2018. Exploiting The Laws of Order in Smart Contracts. CoRR abs\/1810.11605 ( 2018 ). arXiv: 1810.11605 Aashish Kolluri, Ivica Nikoli\u0107, Ilya Sergey, Aquinas Hobor, and Prateek Saxena. 2018. Exploiting The Laws of Order in Smart Contracts. CoRR abs\/1810.11605 (2018). arXiv: 1810.11605"},{"key":"e_1_2_2_48_1","volume-title":"USENIX Security Symposium. USENIX Association, 1317\u20131333","author":"Krupp Johannes","year":"2018","unstructured":"Johannes Krupp and Christian Rossow . 2018 . teEther: Gnawing at Ethereum to Automatically Exploit Smart Contracts . In USENIX Security Symposium. USENIX Association, 1317\u20131333 . Johannes Krupp and Christian Rossow. 2018. teEther: Gnawing at Ethereum to Automatically Exploit Smart Contracts. In USENIX Security Symposium. USENIX Association, 1317\u20131333."},{"key":"e_1_2_2_49_1","doi-asserted-by":"crossref","unstructured":"Ramana Kumar Magnus O. Myreen Michael Norrish and Scott Owens. 2014. CakeML: a verified implementation of ML. In POPL. ACM 179\u2013192.  Ramana Kumar Magnus O. Myreen Michael Norrish and Scott Owens. 2014. CakeML: a verified implementation of ML. In POPL. ACM 179\u2013192.","DOI":"10.1145\/2578855.2535841"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/604174.604179"},{"key":"e_1_2_2_51_1","volume-title":"Proceedings of the ACM SIGPLAN 1994 Conference on Programming Language Design and Implementation (PLDI). ACM, 24\u201335","author":"Launchbury John","unstructured":"John Launchbury and Simon L . Peyton Jones. 1994. Lazy Functional State Threads . In Proceedings of the ACM SIGPLAN 1994 Conference on Programming Language Design and Implementation (PLDI). ACM, 24\u201335 . John Launchbury and Simon L. Peyton Jones. 1994. Lazy Functional State Threads. In Proceedings of the ACM SIGPLAN 1994 Conference on Programming Language Design and Implementation (PLDI). ACM, 24\u201335."},{"key":"e_1_2_2_52_1","doi-asserted-by":"crossref","unstructured":"James J. Leifer Gilles Peskine Peter Sewell and Keith Wansbrough. 2003. Global abstraction-safe marshalling with hash types. In ICFP. ACM 87\u201398.  James J. Leifer Gilles Peskine Peter Sewell and Keith Wansbrough. 2003. Global abstraction-safe marshalling with hash types. In ICFP. ACM 87\u201398.","DOI":"10.1145\/944746.944714"},{"key":"e_1_2_2_53_1","volume-title":"Jones","author":"Liang Sheng","year":"1995","unstructured":"Sheng Liang , Paul Hudak , and Mark P . Jones . 1995 . Monad Transformers and Modular Interpreters. In POPL. ACM Press , 333\u2013343. Sheng Liang, Paul Hudak, and Mark P. Jones. 1995. Monad Transformers and Modular Interpreters. In POPL. ACM Press, 333\u2013343."},{"key":"e_1_2_2_54_1","unstructured":"LSP 2018. Language Server Protocol. https:\/\/langserver.org .  LSP 2018. Language Server Protocol. https:\/\/langserver.org ."},{"key":"e_1_2_2_55_1","doi-asserted-by":"crossref","unstructured":"Loi Luu Duc-Hiep Chu Hrishi Olickel Prateek Saxena and Aquinas Hobor. 2016. Making Smart Contracts Smarter. In CCS. ACM 254\u2013269.  Loi Luu Duc-Hiep Chu Hrishi Olickel Prateek Saxena and Aquinas Hobor. 2016. Making Smart Contracts Smarter. In CCS. ACM 254\u2013269.","DOI":"10.1145\/2976749.2978309"},{"key":"e_1_2_2_56_1","first-page":"219","article-title":"An Introduction to Input\/Output Automata","volume":"2","author":"Lynch Nancy A.","year":"1989","unstructured":"Nancy A. Lynch and Mark R. Tuttle . 1989 . An Introduction to Input\/Output Automata . CWI Quarterly 2 (1989), 219 \u2013 246 . Nancy A. Lynch and Mark R. Tuttle. 1989. An Introduction to Input\/Output Automata. CWI Quarterly 2 (1989), 219\u2013246.","journal-title":"CWI Quarterly"},{"key":"e_1_2_2_57_1","volume-title":"ISoLA (LNCS)","author":"Marescotti Matteo","unstructured":"Matteo Marescotti , Martin Blicha , Antti E. J. Hyv\u00e4rinen , Sepideh Asadi , and Natasha Sharygina . 2018. Computing Exact Worst-Case Gas Consumption for Smart Contracts . In ISoLA (LNCS) , Vol. 11247 . Springer , 450\u2013465. Matteo Marescotti, Martin Blicha, Antti E. J. Hyv\u00e4rinen, Sepideh Asadi, and Natasha Sharygina. 2018. Computing Exact Worst-Case Gas Consumption for Smart Contracts. In ISoLA (LNCS), Vol. 11247. Springer, 450\u2013465."},{"key":"e_1_2_2_58_1","unstructured":"Yaron Minsky. 2016. Let syntax and why you should use it. Blog post available at https:\/\/blog.janestreet.com\/let-syntaxand-why-you-should-use-it .  Yaron Minsky. 2016. Let syntax and why you should use it. Blog post available at https:\/\/blog.janestreet.com\/let-syntaxand-why-you-should-use-it ."},{"key":"e_1_2_2_59_1","volume-title":"Concepts in programming languages","author":"Mitchell John C.","unstructured":"John C. Mitchell . 2003. Concepts in programming languages . Cambridge University Press . John C. Mitchell. 2003. Concepts in programming languages. Cambridge University Press."},{"key":"e_1_2_2_60_1","unstructured":"Steven S. Muchnick. 1997. Advanced Compiler Design and Implementation. Morgan Kaufmann.  Steven S. Muchnick. 1997. Advanced Compiler Design and Implementation. Morgan Kaufmann."},{"key":"e_1_2_2_61_1","volume-title":"Bitcoin: A peer-to-peer electronic cash system. Abailable at http:\/\/bitcoin.org\/bitcoin.pdf .","author":"Nakamoto Satoshi","year":"2008","unstructured":"Satoshi Nakamoto . 2008 . Bitcoin: A peer-to-peer electronic cash system. Abailable at http:\/\/bitcoin.org\/bitcoin.pdf . Satoshi Nakamoto. 2008. Bitcoin: A peer-to-peer electronic cash system. Abailable at http:\/\/bitcoin.org\/bitcoin.pdf ."},{"key":"e_1_2_2_62_1","doi-asserted-by":"crossref","unstructured":"Ivica Nikoli\u0107 Aashish Kolluri Ilya Sergey Prateek Saxena and Aquinas Hobor. 2018. Finding The Greedy Prodigal and Suicidal Contracts at Scale. In ACSAC. ACM. To appear.  Ivica Nikoli\u0107 Aashish Kolluri Ilya Sergey Prateek Saxena and Aquinas Hobor. 2018. Finding The Greedy Prodigal and Suicidal Contracts at Scale. In ACSAC. ACM. To appear.","DOI":"10.1145\/3274694.3274743"},{"key":"e_1_2_2_63_1","volume-title":"Simplicity: A New Language for Blockchains. https:\/\/blockstream.com\/simplicity.pdf .","author":"O\u2019Connor Russell","year":"2017","unstructured":"Russell O\u2019Connor . 2017 . Simplicity: A New Language for Blockchains. https:\/\/blockstream.com\/simplicity.pdf . Russell O\u2019Connor. 2017. Simplicity: A New Language for Blockchains. https:\/\/blockstream.com\/simplicity.pdf ."},{"key":"e_1_2_2_64_1","volume-title":"ESOP (LNCS)","author":"Owens Scott","unstructured":"Scott Owens , Magnus O. Myreen , Ramana Kumar , and Yong Kiam Tan . 2016. Functional Big-Step Semantics . In ESOP (LNCS) , Vol. 9632 . Springer , 589\u2013615. Scott Owens, Magnus O. Myreen, Ramana Kumar, and Yong Kiam Tan. 2016. Functional Big-Step Semantics. In ESOP (LNCS), Vol. 9632. Springer, 589\u2013615."},{"key":"e_1_2_2_65_1","volume-title":"The Implementation of Functional Programming Languages","author":"Peyton Jones Simon L.","unstructured":"Simon L. Peyton Jones . 1987. The Implementation of Functional Programming Languages . Prentice-Hall . Simon L. Peyton Jones. 1987. The Implementation of Functional Programming Languages. Prentice-Hall."},{"key":"e_1_2_2_66_1","volume-title":"TLCA (LNCS)","author":"Peyton Jones Simon L.","unstructured":"Simon L. Peyton Jones . 2013. Type-Directed Compilation in the Wild: Haskell and Core . In TLCA (LNCS) , Vol. 7941 . Springer . Simon L. Peyton Jones. 2013. Type-Directed Compilation in the Wild: Haskell and Core. In TLCA (LNCS), Vol. 7941. Springer."},{"key":"e_1_2_2_67_1","doi-asserted-by":"crossref","unstructured":"George P\u00eerlea and Ilya Sergey. 2018. Mechanising Blockchain Consensus. In CPP. ACM 78\u201390.  George P\u00eerlea and Ilya Sergey. 2018. Mechanising Blockchain Consensus. In CPP. ACM 78\u201390.","DOI":"10.1145\/3176245.3167086"},{"key":"e_1_2_2_68_1","volume-title":"Implicit Syntax. In Informal Proceedings of First Workshop on Logical Frameworks, Antibes.","author":"Pollack Robert","year":"1990","unstructured":"Robert Pollack . 1990 . Implicit Syntax. In Informal Proceedings of First Workshop on Logical Frameworks, Antibes. Robert Pollack. 1990. Implicit Syntax. In Informal Proceedings of First Workshop on Logical Frameworks, Antibes."},{"key":"e_1_2_2_69_1","unstructured":"Stuart Popejoy. 2017. The Pact Smart-Contract Language Revision 1.5. http:\/\/kadena.io\/docs\/Kadena-PactWhitepaper.pdf .  Stuart Popejoy. 2017. The Pact Smart-Contract Language Revision 1.5. http:\/\/kadena.io\/docs\/Kadena-PactWhitepaper.pdf ."},{"key":"e_1_2_2_70_1","unstructured":"RChain Cooperative. 2019. Rholang. https:\/\/rholang.rchain.coop .  RChain Cooperative. 2019. Rholang. https:\/\/rholang.rchain.coop ."},{"key":"e_1_2_2_71_1","unstructured":"Christian Reitwiessner. 2017. Babbage\u2014a mechanical smart contract language. Online blog post.  Christian Reitwiessner. 2017. Babbage\u2014a mechanical smart contract language. Online blog post."},{"key":"e_1_2_2_72_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-06859-7_148"},{"key":"e_1_2_2_73_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1010027404223"},{"key":"e_1_2_2_74_1","volume-title":"Sereum: Protecting Existing Smart Contracts Against Re-Entrancy Attacks. In NDSS.","author":"Rodler Michael","year":"2019","unstructured":"Michael Rodler , Wenting Li , Ghassan O. Karame , and Lucas Davi . 2019 . Sereum: Protecting Existing Smart Contracts Against Re-Entrancy Attacks. In NDSS. Michael Rodler, Wenting Li, Ghassan O. Karame, and Lucas Davi. 2019. Sereum: Protecting Existing Smart Contracts Against Re-Entrancy Attacks. In NDSS."},{"key":"e_1_2_2_75_1","volume-title":"IELE: A New Virtual Machine for the Blockchain. https:\/\/iohk.io\/blog\/iele-a-new-virtual-machine-forthe-blockchain .","author":"Rosu Grigore","year":"2018","unstructured":"Grigore Rosu . 2018 . IELE: A New Virtual Machine for the Blockchain. https:\/\/iohk.io\/blog\/iele-a-new-virtual-machine-forthe-blockchain . Grigore Rosu. 2018. IELE: A New Virtual Machine for the Blockchain. https:\/\/iohk.io\/blog\/iele-a-new-virtual-machine-forthe-blockchain ."},{"key":"e_1_2_2_76_1","volume-title":"Writing Safe Smart Contracts in Flint. Master\u2019s thesis","author":"Schrans Franklin","unstructured":"Franklin Schrans . 2018. Writing Safe Smart Contracts in Flint. Master\u2019s thesis . Imperial College London , Department of Computing. Franklin Schrans. 2018. Writing Safe Smart Contracts in Flint. Master\u2019s thesis. Imperial College London, Department of Computing."},{"key":"e_1_2_2_77_1","volume-title":"Writing safe smart contracts in Flint. In &lt;Programming&gt","author":"Schrans Franklin","unstructured":"Franklin Schrans , Susan Eisenbach , and Sophia Drossopoulou . 2018. Writing safe smart contracts in Flint. In &lt;Programming&gt ; (Companion). ACM , 218\u2013219. Franklin Schrans, Susan Eisenbach, and Sophia Drossopoulou. 2018. Writing safe smart contracts in Flint. In &lt;Programming&gt; (Companion). ACM, 218\u2013219."},{"key":"e_1_2_2_78_1","doi-asserted-by":"crossref","unstructured":"Ilya Sergey Dominique Devriese Matthew Might Jan Midtgaard David Darais Dave Clarke and Frank Piessens. 2013. Monadic Abstract Interpreters. In PLDI. ACM 399\u2013410.  Ilya Sergey Dominique Devriese Matthew Might Jan Midtgaard David Darais Dave Clarke and Frank Piessens. 2013. Monadic Abstract Interpreters. In PLDI. ACM 399\u2013410.","DOI":"10.1145\/2499370.2491979"},{"key":"e_1_2_2_79_1","volume-title":"Scilla: a Smart Contract Intermediate-Level LAnguage. CoRR abs\/1801.00687","author":"Sergey Ilya","year":"2018","unstructured":"Ilya Sergey , Amrit Kumar , and Aquinas Hobor . 2018a. Scilla: a Smart Contract Intermediate-Level LAnguage. CoRR abs\/1801.00687 ( 2018 ). http:\/\/arxiv.org\/abs\/1801.00687 Ilya Sergey, Amrit Kumar, and Aquinas Hobor. 2018a. Scilla: a Smart Contract Intermediate-Level LAnguage. CoRR abs\/1801.00687 (2018). http:\/\/arxiv.org\/abs\/1801.00687"},{"key":"e_1_2_2_80_1","volume-title":"ISoLA (LNCS)","author":"Sergey Ilya","unstructured":"Ilya Sergey , Amrit Kumar , and Aquinas Hobor . 2018b. Temporal Properties of Smart Contracts . In ISoLA (LNCS) , Vol. 11247 . Springer , 323\u2013338. Ilya Sergey, Amrit Kumar, and Aquinas Hobor. 2018b. Temporal Properties of Smart Contracts. In ISoLA (LNCS), Vol. 11247. Springer, 323\u2013338."},{"key":"e_1_2_2_81_1","volume-title":"Peyton Jones","author":"Sergey Ilya","year":"2014","unstructured":"Ilya Sergey , Dimitrios Vytiniotis , and Simon L . Peyton Jones . 2014 . Modular, higher-order cardinality analysis in theory and practice. In POPL. ACM , 335\u2013348. Ilya Sergey, Dimitrios Vytiniotis, and Simon L. Peyton Jones. 2014. Modular, higher-order cardinality analysis in theory and practice. In POPL. ACM, 335\u2013348."},{"key":"e_1_2_2_82_1","volume-title":"International Seminar on Partial Evaluation, Dagstuhl Castle (LNCS)","author":"Sestoft Peter","unstructured":"Peter Sestoft . 1996. ML Pattern Match Compilation and Partial Evaluation . In International Seminar on Partial Evaluation, Dagstuhl Castle (LNCS) , Vol. 1110 . Springer , 446\u2013464. Peter Sestoft. 1996. ML Pattern Match Compilation and Partial Evaluation. In International Seminar on Partial Evaluation, Dagstuhl Castle (LNCS), Vol. 1110. Springer, 446\u2013464."},{"key":"e_1_2_2_83_1","volume-title":"Cook","author":"Shali Amin","year":"2011","unstructured":"Amin Shali and William R . Cook . 2011 . Hybrid Partial Evaluation. In OOPSLA. ACM , 375\u2013390. Amin Shali and William R. Cook. 2011. Hybrid Partial Evaluation. In OOPSLA. ACM, 375\u2013390."},{"key":"e_1_2_2_84_1","unstructured":"Dieter Shirley. 2018. ERC-721. http:\/\/erc721.org\/ .  Dieter Shirley. 2018. ERC-721. http:\/\/erc721.org\/ ."},{"key":"e_1_2_2_85_1","unstructured":"Jeremy Siek. 2012. Big-step diverging or stuck? http:\/\/siek.blogspot.com\/2012\/07\/big-step-diverging-or-stuck.html .  Jeremy Siek. 2012. Big-step diverging or stuck? http:\/\/siek.blogspot.com\/2012\/07\/big-step-diverging-or-stuck.html ."},{"key":"e_1_2_2_86_1","unstructured":"Jeremy Siek. 2013. Type safety in three easy lemmas. http:\/\/siek.blogspot.com\/2013\/05\/type-safety-in-three-easylemmas.html .  Jeremy Siek. 2013. Type safety in three easy lemmas. http:\/\/siek.blogspot.com\/2013\/05\/type-safety-in-three-easylemmas.html ."},{"key":"e_1_2_2_87_1","unstructured":"Flora Sun. 2018. UTXO vs Account\/Balance Model. Online blog post available at https:\/\/medium.com\/@sunflora98\/utxovs-account-balance-model-5e6470f4e0cf .  Flora Sun. 2018. UTXO vs Account\/Balance Model. Online blog post available at https:\/\/medium.com\/@sunflora98\/utxovs-account-balance-model-5e6470f4e0cf ."},{"key":"e_1_2_2_88_1","unstructured":"Nick Szabo. 1994. Smart Contracts. Online manuscript.  Nick Szabo. 1994. Smart Contracts. Online manuscript."},{"key":"e_1_2_2_89_1","unstructured":"Tezos Foundation. 2018a. Michelson: the language of Smart Contracts in Tezos. http:\/\/tezos.gitlab.io\/mainnet\/whitedoc\/ michelson.html .  Tezos Foundation. 2018a. Michelson: the language of Smart Contracts in Tezos. http:\/\/tezos.gitlab.io\/mainnet\/whitedoc\/ michelson.html ."},{"key":"e_1_2_2_90_1","unstructured":"Tezos Foundation. 2018b. Liquidity. http:\/\/www.liquidity-lang.org\/ .  Tezos Foundation. 2018b. Liquidity. http:\/\/www.liquidity-lang.org\/ ."},{"key":"e_1_2_2_91_1","doi-asserted-by":"crossref","unstructured":"Sergei Tikhomirov Ekaterina Voskresenskaya Ivan Ivanitskiy Ramil Takhaviev Evgeny Marchenko and Yaroslav Alexandrov. 2018. SmartCheck: Static Analysis of Ethereum Smart Contracts. In WETSEB@ICSE. ACM 9\u201316.  Sergei Tikhomirov Ekaterina Voskresenskaya Ivan Ivanitskiy Ramil Takhaviev Evgeny Marchenko and Yaroslav Alexandrov. 2018. SmartCheck: Static Analysis of Ethereum Smart Contracts. In WETSEB@ICSE. ACM 9\u201316.","DOI":"10.1145\/3194113.3194115"},{"key":"e_1_2_2_92_1","unstructured":"Anton Trunov. 2019. A Scilla vs Move case study. Blog post available at https:\/\/medium.com\/@anton_trunov\/a-scilla-vsmove-case-study-afa9b8df5146 .  Anton Trunov. 2019. A Scilla vs Move case study. Blog post available at https:\/\/medium.com\/@anton_trunov\/a-scilla-vsmove-case-study-afa9b8df5146 ."},{"key":"e_1_2_2_93_1","volume-title":"Dana Drachsler-Cohen, Arthur Gervais, Florian B\u00fcnzli, and Martin T. Vechev.","author":"Tsankov Petar","year":"2018","unstructured":"Petar Tsankov , Andrei Marian Dan , Dana Drachsler-Cohen, Arthur Gervais, Florian B\u00fcnzli, and Martin T. Vechev. 2018 . Securify : Practical Security Analysis of Smart Contracts. In CCS. ACM , 67\u201382. Petar Tsankov, Andrei Marian Dan, Dana Drachsler-Cohen, Arthur Gervais, Florian B\u00fcnzli, and Martin T. Vechev. 2018. Securify: Practical Security Analysis of Smart Contracts. In CCS. ACM, 67\u201382."},{"key":"e_1_2_2_95_1","volume-title":"Ethereum: A Secure Decentralized Generalised Transaction Ledger.","author":"Wood Gavin","year":"2014","unstructured":"Gavin Wood . 2014 . Ethereum: A Secure Decentralized Generalised Transaction Ledger. Gavin Wood. 2014. Ethereum: A Secure Decentralized Generalised Transaction Ledger."},{"key":"e_1_2_2_96_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"},{"key":"e_1_2_2_97_1","unstructured":"Zilliqa Team. 2017. The Zilliqa Technical Whitepaper. https:\/\/docs.zilliqa.com\/whitepaper.pdf Version 0.1.  Zilliqa Team. 2017. The Zilliqa Technical Whitepaper. https:\/\/docs.zilliqa.com\/whitepaper.pdf Version 0.1."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360611","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3360611","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:22:59Z","timestamp":1750202579000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360611"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10,10]]},"references-count":95,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2019,10,10]]}},"alternative-id":["10.1145\/3360611"],"URL":"https:\/\/doi.org\/10.1145\/3360611","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,10,10]]},"assertion":[{"value":"2019-10-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}