IMDEA Software

Iniciativa IMDEA

Inicio > Eventos > Charlas Invitadas > 2019 > Designing Dijkstra Monads
Esta página aún no ha sido traducida. A continuación se muestra la página en inglés.

Kenji Maillard

miércoles 10 de abril de 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.