Dijkstra Monads for Free

Danel Ahman, Catalin Hritcu, Kenji Maillard, Guido Martínez, Gordon Plotkin, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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*.
Original languageEnglish
Title of host publicationProceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages
PublisherACM
Pages515-529
Number of pages15
ISBN (Electronic)978-1-4503-4660-3
DOIs
Publication statusPublished - 1 Jan 2017
Event44th ACM SIGPLAN Symposium on Principles of Programming Languages 2017 - Paris, France
Duration: 15 Jan 201721 Jan 2017
https://conf.researchr.org/home/POPL-2017

Publication series

NameACM SIGPLAN Notices
PublisherACM
Number1
Volume52
ISSN (Print)0362-1340
ISSN (Electronic)1558-1160

Conference

Conference44th ACM SIGPLAN Symposium on Principles of Programming Languages 2017
Abbreviated titlePOPL 2017
CountryFrance
CityParis
Period15/01/1721/01/17
Internet address

Fingerprint Dive into the research topics of 'Dijkstra Monads for Free'. Together they form a unique fingerprint.

Cite this