IMDEA Software

IMDEA initiative

Home > Events > Invited Talks > 2019 > Designing Dijkstra Monads

Kenji Maillard

Wednesday, April 10, 2019

2:45pm Meeting room 302 (Mountain View), level 3

Kenji Maillard, PhD Student, INRIA Paris, France

Designing Dijkstra Monads


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.