Tue 19 Jun 2018 16:15 - 16:20 at Columbus Ballroom B - Lightning Talks

Blockchain protocols, including Bitcoin and Ethereum, allow for programmable transactions that determine for whom, when, and how funds can be redeemed. This lets users create “smart contracts” where conditions and obligations for transactions are enforced by the protocol itself. Unfortunately, hundreds of millions of dollars worth of Ethereum funds have already been lost due to programming errors in smart contracts. Ultimately, smart contracts will need to securely manage the irreversible transfer of millions of dollars worth of funds using custom, one-shot contracts, that are executed in the adversarial environment of the public internet. To achieve this, we are developing Simplicity, a new programming language designed for blockchains. Using the Coq proof assistant, we have developed both functional and operational formal semantics for our combinator-based language. We intend to use the VST to prove our C interpreter meets our formal semantics. Our goal is to use Deep Specifications to ensure smart contracts meet their design specifications and are executed correctly by the actual machine code that implements their protocols. Details about Simplicity can be found at https://arxiv.org/abs/1711.03028 or https://blockstream.com/simplicity.pdf.

Tue 19 Jun

deepspec-2018-papers
16:10 - 17:35: DeepSpec 2018 - Lightning Talks at Columbus Ballroom B
deepspec-2018-papers16:10 - 16:15
Talk
deepspec-2018-papers16:15 - 16:20
Talk
deepspec-2018-papers16:20 - 16:25
Talk
Gordon StewartOhio University
deepspec-2018-papers16:25 - 16:30
Talk
deepspec-2018-papers16:30 - 16:35
Talk
deepspec-2018-papers16:35 - 16:40
Talk
deepspec-2018-papers16:40 - 16:45
Talk
Christine RizkallahUniversity of New South Wales
deepspec-2018-papers16:45 - 16:50
Talk
Joonwon ChoiMassachusetts Institute of Technology, USA
deepspec-2018-papers16:50 - 16:55
Talk
Sam GruetterMassachusetts Institute of Technology