Dijkstra Monads for Free

Dijkstra Monads for Free

Artifact Evaluation Badge

Danel Ahman1,2    Cătălin Hriţcu1,3    Kenji Maillard1,3,4    Guido Martínez3,5
Gordon Plotkin1,2    Jonathan Protzenko1    Aseem Rastogi1    Nikhil Swamy1

1Microsoft Research    2University of Edinburgh    3Inria Paris    4ENS Paris    5Rosario National University

Symposium on Principles of Programming Languages, POPL 2017

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 system, EMF⭑ enables a novel mixture of intrinsic and extrinsic proofs within F⭑.