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

We integrate static and dynamic contract-based verification of stateful programs. Although contracts are useful to reason about programs, naive introduction of mutable references makes the reasoning difficult because state-dependent contracts that have been successfully checked can be invalidated by state mutation. The problem is more acute in manifest contract systems, in which contracts are part of static types, in that the naive introduction of assignments would break their important soundness properties.

We address this problem by designing a manifest contract system where specifications of pure code fragments are represented by refinement types and specifications of impure ones are by computational Hoare types—a variant of Nanevski et al’s Hoare types—which express pre- and postconditions of stateful computations in the same language as programs. To prevent troubles caused by abusing references in contracts, we introduce a region-based effect system, which allows contracts in refinement types and Hoare types to manipulate references as long as they are observationally pure and read-only, respectively. We show that our calculus has the same kind of soundness property as existing pure manifest calculi and, furthermore, stateful computations satisfy their postconditions if they terminate without dynamic contract violation.

Following Belo et al., static verification in this work is ``post facto'', that is, we define the manifest contract system so that all contracts are checked at run time, formalize what dynamic checks can be eliminated safely, and show that programs with and without such checks are contextually equivalent—intuitively, checks of contracts can be eliminated when their satisfaction is derived from other, already established contracts. We also apply the idea of post facto verification to region-based local reasoning, which shows that satisfaction of preconditions which do not refer to references mutated by a computation is preserved even after executing the computation.

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