Write a Blog >>
Sun 20 - Fri 25 October 2019 Athens, Greece
Thu 24 Oct 2019 11:45 - 12:07 at Attica - Language Design Chair(s): Tiark Rompf

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.

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.

Thu 24 Oct
Times are displayed in time zone: Beirut change

11:00 - 12:30: Language DesignOOPSLA at Attica
Chair(s): Tiark RompfPurdue University
11:00 - 11:22
DeepSEA: A Language for Certified System Software
Vilhelm SjöbergYale University, Yuyang SangYale University, Shu-chun WengYale University, Zhong ShaoYale University
DOI Pre-print
11:22 - 11:45
Weakening WebAssembly
Conrad WattUniversity of Cambridge, Andreas RossbergDfinity Stiftung, Jean Pichon-PharabodUniversity of Cambridge
11:45 - 12:07
Safer Smart Contract Programming with Scilla
Ilya SergeyYale-NUS College and National University of Singapore, Vaivaswatha NagarajZilliqa Research, Jacob JohannsenZilliqa Research, Amrit KumarZilliqa Research, Anton TrunovZilliqa Research, Ken ChanZilliqa Research
DOI Pre-print File Attached
12:07 - 12:30
Scala Implicits Are Everywhere: A Large-Scale Study of the Use of Scala Implicits in the Wild
Filip KřikavaCzech Technical University, Heather MillerCarnegie Mellon University, Jan VitekNortheastern University
DOI Pre-print