Dijkstra Monads for Free
Résumé
Dijkstra monads are a means by which a dependent type theory can be
enhanced with support for reasoning about effectful code. These
specification-level monads computing weakest preconditions, and their
closely related counterparts, Hoare monads, provide the basis on which
verification tools like F*, Hoare Type Theory (HTT), and Ynot are
built. In this paper we show that Dijkstra monads can be derived "for
free" by applying a continuation-passing style (CPS) translation to
the standard monadic definitions of the underlying computational effects.
Automatically deriving Dijkstra monads provides a
correct-by-construction and efficient way of reasoning about
user-defined effects in dependent type theories. We demonstrate these
ideas in EMF*, a new dependently typed calculus, validating it both by
formal proof and via a prototype implementation within F*. Besides
equipping F* with a more uniform and extensible effect system, EMF*
enables within F* a mixture of intrinsic and extrinsic proofs that was
previously impossible.