An attempt at modeling various Lattices and CRDTs in Coq and Haskell.
JoinSemiLattice.v: An experiment in modeling JoinSemiLattices over naturals as outlined by Conway.Counters.v: Work in modeling CvRDTs, specifically G-Counters and PN-Counters as outlined by Shapiro.
- The current record definiton for CvRDTs does not support multiple update functions. This needs to somehow be adapted for allowing multiple update functions to exist for a given CvRDT. Not sure how to do this.
- How do we use these records for defining and overall signature for CvRDTS?
- Conway, Marczak, Alvaro, Hellerstein, Maier, Logic and Lattices in Distributed Programming
- Shapiro, Preguiça, Baquero, Zawirski, A comprehensive study of Convergent and Commutative Replicated Data Types
Copyright (C) 2013 Christopher Meiklejohn.