POPL 2017
Sun 15 - Sat 21 January 2017
Thu 19 Jan 2017 15:10 - 15:35 at Auditorium - Functional Programming with Effects Chair(s): Kathleen Fisher

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*.

Thu 19 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

14:20 - 16:00
Functional Programming with EffectsPOPL at Auditorium
Chair(s): Kathleen Fisher Tufts University
14:20
25m
Talk
Type Directed Compilation of Row-Typed Algebraic Effects
POPL
Daan Leijen Microsoft Research
14:45
25m
Talk
Do be do be do
POPL
Sam Lindley University of Edinburgh, Conor McBride , Craig McLaughlin The University of Edinburgh
15:10
25m
Talk
Dijkstra Monads for Free
POPL
Danel Ahman University of Edinburgh, Cătălin Hriţcu Inria Paris, Kenji Maillard Inria Paris, ENS Paris, and Microsoft Research, Guido Martínez CIFASIS-CONICET, Argentina, Gordon Plotkin , Jonathan Protzenko Microsoft Research, Aseem Rastogi Microsoft Research India, Nikhil Swamy Microsoft Research
Pre-print
15:35
25m
Talk
Stateful Manifest Contracts
POPL
Taro Sekiyama , Atsushi Igarashi Kyoto University