Blogs (28) >>
ICFP 2017
Sun 3 - Sat 9 September 2017 Oxford, United Kingdom
Sat 9 Sep 2017 14:00 - 14:25 at L2 - CUFP Talks 4

Digital Asset builds distributed-ledger and smart-contract technology for enterprise applications. Two key promises of this technology are significantly lower operational costs and increased auditability. Key techniques to realize these promises are the representation of contracts as code and immutable, authenticated data-structures. However, these techniques also do require significantly higher correctness guarantees from both contract specifications and ledger implementations. At Digital Asset, we provide these correctness guarantees by systematically applying formal methods.

In this talk, I’ll give insights into one such application of formal methods. More precisely, I’ll explain how we use Isabelle/HOL to provide a verified implementation of the interpreter for DAML, our smart-contract language. The goal of this talk is to show how one can leverage Isabelle/HOL as a combined implementation and verification environment for core algorithms.

Sat 9 Sep

Displayed time zone: Belfast change

14:00 - 14:50
CUFP Talks 4CUFP at L2
Formally Verifying a Smart-Contract Language Implementation with Isabelle
Simon Meier Digital Asset
Haskell games and apps for iOS and Android
Ivan Perez University of Nottingham, UK