Attending this event?
View analytic
Saturday, November 17 • 3:00pm - 3:40pm
Simplicity for Programmable Money

Sign up or log in to save this to your schedule and see who's attending!

Imagine taking your favourite functional programming language and removing recursion, recursive types, and even removing function types. What do you have left? Everything you need for programmable money! Simplicity is a new typed, combinator-based, functional language without loops and recursion, designed to be used within crypto-currencies and blockchain applications. Simplicity comes with formal semantics defined using Coq, a popular, general purpose software proof assistant based on dependent type theory. In this presentation I will describe the Simplicity language. I will demonstrate how to write some small programs in Simplicity and show how to use Coq to prove that they behave correctly.

avatar for Russell O'Connor

Russell O'Connor

Software Developer, Blockstream
Lazy functional programing a la Haskell. | Developed lens-family and mezzolens Haskell libraries | | Dependently typed programming and proofs a la Coq. | Worked on Galois theory proofs for the verification of the Feit-Thompson theorem. | | Running NixOS on my laptop since 2010... Read More →

Saturday November 17, 2018 3:00pm - 3:40pm

Twitter Feed