Write a Blog >>
ICFP 2019
Sun 18 - Fri 23 August 2019 Berlin, Germany
Wed 21 Aug 2019 11:37 - 12:00 at Aurora Borealis - Program Verification Chair(s): Adam Chlipala

We introduce Carol, a refinement-typed programming language for replicated data stores. The salient feature of Carol is that it allows programming and verifying replicated store operations modularly, without consideration of other operations that might interleave, and sequentially, without requiring reference to or knowledge of the concurrent execution model. This is in stark contrast with existing systems, which require understanding the concurrent interactions of all pairs of operations when developing or verifying them.

The key enabling idea is the consistency guard, a two-state predicate relating the locally-viewed store and the hypothetical remote store that an operation’s updates may eventually be applied to, which is used by the Carol programmer to declare their precise consistency requirements. Guards appear to the programmer and refinement typechecker as simple data pre-conditions, enabling sequential reasoning, while appearing to the distributed runtime as consistency control instructions.

We implement and evaluate the Carol system in two parts: (1) the algorithm used to statically translate guards into the runtime coordination actions required to enforce them, and (2) the networked-replica runtime which executes arbitrary operations, written in a Haskell DSL, according to the Carol language semantics.

Wed 21 Aug
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:00: Program VerificationResearch Papers at Aurora Borealis
Chair(s): Adam ChlipalaMassachusetts Institute of Technology
10:30 - 10:52
A predicate transformer semantics for effects (Functional Pearl)
Research Papers
Wouter SwierstraUtrecht University, Netherlands, Tim BaanenUtrecht University
10:52 - 11:15
Dijkstra Monads for All
Research Papers
Kenji MaillardInria Paris and ENS Paris, Danel AhmanUniversity of Ljubljana, Robert AtkeyUniversity of Strathclyde, Guido MartínezCIFASIS-CONICET, Argentina, Cătălin HriţcuInria Paris, Exequiel RivasInria Paris, Éric TanterUniversity of Chile & Inria Paris
11:15 - 11:37
Mechanized Relational Verification of Concurrent Programs with Continuations
Research Papers
Amin Timanyimec-Distrinet KU-Leuven, Lars BirkedalAarhus University
11:37 - 12:00
Sequential Programming for Replicated Data Stores
Research Papers
Nicholas V. LewchenkoUniversity of Colorado Boulder, Arjun RadhakrishnaMicrosoft, Akash Gaonkar, Pavol CernyUniversity of Colorado Boulder
DOI Pre-print