Dijkstra Monads for Free
Danel Ahman, Catalin Hritcu, Kenji Maillard, Guido Martinez, and Gordon Plotkin, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy

TL;DR
This paper introduces a method to automatically derive Dijkstra monads for effectful computations using CPS translation, enhancing dependent type theories with verified effect reasoning.
Contribution
It presents a novel approach to derive Dijkstra monads automatically, improving effect reasoning in dependent type theories and implementing it in EMF* for practical validation.
Findings
Automatic derivation of Dijkstra monads is correct and efficient.
EMF* extends F* with a more uniform effect system.
Supports intrinsic and extrinsic proofs within F*.
Abstract
Dijkstra monads enable a dependent type theory to be enhanced with support for specifying and verifying effectful code via weakest preconditions. Together with their closely related counterparts, Hoare monads, they provide the basis on which verification tools like F*, Hoare Type Theory (HTT), and Ynot are built. 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 in this way 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 via both formal proof and a prototype implementation within F*. Besides equipping F* with a more uniform and extensible effect…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
