CONICET | Buscador de Institutos y Recursos Humanos

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.