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
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

14:20 - 16:00: Functional Programming with EffectsPOPL at Auditorium
Chair(s): Kathleen FisherTufts University
14:20 - 14:45
Type Directed Compilation of Row-Typed Algebraic Effects
Daan LeijenMicrosoft Research
14:45 - 15:10
Do be do be do
Sam LindleyUniversity of Edinburgh, Conor McBride, Craig McLaughlinThe University of Edinburgh
15:10 - 15:35
Dijkstra Monads for Free
Danel AhmanUniversity of Edinburgh, Cătălin HriţcuInria Paris, Kenji MaillardInria Paris, ENS Paris, and Microsoft Research, Guido MartínezCIFASIS-CONICET, Argentina, Gordon Plotkin, Jonathan ProtzenkoMicrosoft Research, Aseem RastogiMicrosoft Research India, Nikhil SwamyMicrosoft Research
15:35 - 16:00
Stateful Manifest Contracts