An Implementation of the operational semantics of weakly consistent data-sotres and the declarative isolation and consistency guarantees introduced in PLDI'15 paper Declarative Programming over Eventually Consistent Data Stores (http://gowthamk.github.io/docs/quelea.pdf) in Coq proof assistant.