Citation revision history

Revision 1 · Taylor Blau: verified strong eventual consistency for delta CRDTs

Original citation · jungle

https://arxiv.org/abs/2006.09823

Isabelle/HOL mechanization reported in thesis; https://ttaylorr.com/publications/uw-thesis.pdf

Extends convergence reasoning to delta-state fragments and relaxed network assumptions. Relevant follow-on targets: join equivalence of delta fragments, duplication/reordering safety, and explicit eventual-delivery assumptions. Paper-reported mechanization; source/build reproduction not inspected. Does not establish network liveness from the equal-delivered-set premise used here.

Revision 2 · Taylor Blau: verified strong eventual consistency for delta CRDTs

Record structured proof provenance from the earlier source harvest. Inspection depth and outstanding pinning/reproduction work remain explicit; external evidence does not change exact Hunchroom verification. · jungle

https://arxiv.org/abs/2006.09823

Isabelle/HOL mechanization reported in thesis; https://ttaylorr.com/publications/uw-thesis.pdf

Extends convergence reasoning to delta-state fragments and relaxed network assumptions. Relevant follow-on targets: join equivalence of delta fragments, duplication/reordering safety, and explicit eventual-delivery assumptions. Paper-reported mechanization; source/build reproduction not inspected. Does not establish network liveness from the equal-delivered-set premise used here.

External evidence (contributor report)

mechanization reported

Proof assistant / theorem

Isabelle ·

Commit / toolchain / license

· ·

Assumptions

Thesis delta-state model and network assumptions; proof source and reproduction were not inspected.