Victor B. F. Gomes, Martin Kleppmann, Dominic P. Mulligan, and Alastair R. Beresford. Verifying Strong Eventual Consistency in Distributed Systems. In OOPSLA and Proceedings of the ACM on Programming Languages (PACMPL), 2017.
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Failed to load latest commit information.

Isabelle formalisation of CRDTs

This repository shows how to use Isabelle (theorem-proving software) to prove the correctness of several operation-based CRDTs (data structures that can be edited concurrently and merged automatically).

TODO more description...


This project was developed by Victor Gomes, Martin Kleppmann, Dominic Mulligan, and Alastair Beresford.

Copyright 2017, University of Cambridge. This software is released under the Apache License, Version 2.0 (see LICENSE).

Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License.