  This paper proposes a general semantic framework for verifying programs with
arbitrary monadic side-effects using Dijkstra monads, which we define as
monad-like structures indexed by a specification monad. We prove that any monad
morphism between a computational monad and a specification monad gives rise to
a Dijkstra monad, which provides great flexibility for obtaining Dijkstra
monads tailored to the verification task at hand. We moreover show that a large
variety of specification monads can be obtained by applying monad transformers
to various base specification monads, including predicate transformers and
Hoare-style pre- and postconditions. For defining correct monad transformers,
we propose a language inspired by Moggi's monadic metalanguage that is
parameterized by a dependent type theory. We also develop a notion of algebraic
operations for Dijkstra monads, and start to investigate two ways of also
accommodating effect handlers. We implement our framework in both Coq and F*,
and illustrate that it supports a wide variety of verification styles for
effects such as exceptions, nondeterminism, state, input-output, and general
recursion.
