ESOP 2015
Tue 14 - Thu 16 April 2015 London, United Kingdom
Thu 16 Apr 2015 11:00 - 11:30 at Skeel - Session 7 Chair(s): Delphine Demange

We propose composite replicated data types, which formalise a common way of organising applications on top of eventually consistent stores. Similarly to a class or an abstract data type, a composite data type encapsulates objects of replicated data types and operations used to access them, implemented using transactions. We develop a method for reasoning about programs with composite data types that reflects their modularity: the method allows abstracting away the internals of composite data type implementations when reasoning about their clients. We express the method as a denotational semantics for a programming language with composite data types. We demonstrate the effectiveness of our semantics by applying it to verify subtle data type examples and prove that it is sound and complete with respect to a standard non-compositional semantics.

Thu 16 Apr

Displayed time zone: Azores change

10:30 - 12:30
Session 7ESOP at Skeel
Chair(s): Delphine Demange IRISA / University of Rennes 1
10:30
30m
Talk
A Semantics for Propositions as Sessions
ESOP
Sam Lindley University of Edinburgh, J. Garrett Morris The University of Edinburgh
11:00
30m
Talk
Composite Replicated Data Types
ESOP
Alexey Gotsman IMDEA, Hongseok Yang University of Oxford
11:30
30m
Talk
Relaxed Stratification: A New Approach to Practical Complete Predicate Refinement
ESOP
Tachio Terauchi JAIST, Hiroshi Unno University of Tsukuba
12:00
30m
Talk
Spatial Interpolants
ESOP
Aws Albarghouthi University of Wisconsin - Madison, Josh Berdine Microsoft Research, Byron Cook Microsoft Research, Zachary Kincaid University of Toronto