Write a Blog >>
SPLASH 2019
Sun 20 - Fri 25 October 2019 Athens, Greece
Thu 24 Oct 2019 16:00 - 16:22 at Olympia - Types Chair(s): Éric Tanter

Programming geo-replicated distributed systems is challenging given the complexity of reasoning about different evolving states on different replicas. Existing approaches to this problem impose significant burden on application developers to consider the effect of how operations performed on one replica are witnessed and applied on others. To alleviate these challenges, we present a fundamentally different approach to programming in the presence of replicated state. Our insight is based on the use of invertible relational specifications of an inductively-defined data type as a mechanism to capture salient aspects of the data type relevant to how its different instances can be safely merged in a replicated environment. Importantly, because these specifications only address a data type's (static) structural properties, their formulation does not require exposing low-level system-level details concerning asynchrony, replication, visibility, etc. As a consequence, our framework enables the correct-by-construction synthesis of rich merge functions over arbitrarily complex (i.e., composable) data types. We show that the use of a rich relational specification language allows us to extract sufficient conditions to automatically derive merge functions that have meaningful non-trivial convergence properties. We incorporate these ideas in a tool called Quark, and demonstrate its utility via a detailed evaluation study on real-world benchmarks.

Conference Day
Thu 24 Oct

Displayed time zone: Beirut change

16:00 - 17:30
TypesOOPSLA at Olympia
Chair(s): Éric TanterUniversity of Chile & Inria Paris
16:00
22m
Talk
Mergeable Replicated Data Types
OOPSLA
Gowtham KakiPurdue University, Swarn PriyaPurdue University, KC SivaramakrishnanIIT Madras, Suresh JagannathanPurdue University
Link to publication DOI
16:22
22m
Talk
Refinement Kinds: Type-Safe Programming with Practical Type-Level Computation
OOPSLA
Luís CairesUniversidade Nova de Lisboa and NOVA LINCS, Bernardo ToninhoUniversidade Nova de Lisboa and NOVA LINCS
DOI
16:45
22m
Talk
System FR: Formalized Foundations for the Stainless Verifier
OOPSLA
Jad HamzaEPFL, Switzerland, Nicolas VoirolEPFL, Switzerland, Viktor KunčakEPFL, Switzerland
DOI
17:07
22m
Talk
Complete Monitors for Gradual Types
OOPSLA
Ben GreenmanPLT @ Northeastern University, Matthias FelleisenPLT @ Northeastern University, Christos DimoulasPLT @ Northwestern University
DOI