Home > Content > Talk by Maria Schett: Blockchain Superoptimizer

Talk by Maria Schett: Blockchain Superoptimizer

Verifying a program consist of proving that a given program meets its
specification. Various frameworks have been studied to provide such
specifications, for instance in Hoare logic programs are specified with pairs of
pre/post-conditions. When dealing with programs mixing a variety of side-effects
such as mutability, divergence, raising exceptions, or non-determinism,
providing a framework for specifying those programs becomes challenging.
Computational monads are a convenient algebraic gadget to uniformly represent a
wide class of such side effects in programming languages. Inspired by Dijkstra's
work, we want to use predicate transformers to verify monadic programs. We will
explain how these predicate transformers can themselves be uniformly represented
as a monad, leading to a powerful verification tool called Dijkstra monads used
heavily in the F* programming language.

Content Source: 
Feed Category: