crdt-isabelle
所属分类：其他
开发工具：TeX
文件大小：0KB
下载次数：0
上传日期：2022-12-18 16:58:43
上 传 者：
sh-1993
说明： 维克多·戈麦斯（Victor B.F.Gomes）、马丁·克莱普曼（Martin Kleppmann）、多米尼克·P.Mulligan和阿拉斯泰尔·贝雷斯福德（Alastair R.Beresford）。正在验证分发中的强最终一致性...，
(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.)
文件列表:
LICENSE (10174, 2022-12-18)
paper/ (0, 2022-12-18)
paper/ACM-Reference-Format.bst (81685, 2022-12-18)
paper/Makefile (742, 2022-12-18)
paper/acmart-pacmpl-template.tex (7495, 2022-12-18)
paper/acmart.cls (83761, 2022-12-18)
paper/appendix.tex (11493, 2022-12-18)
paper/author-response.txt (3095, 2022-12-18)
paper/comment.sty (9200, 2022-12-18)
paper/convergence.tex (19077, 2022-12-18)
paper/happens-before.tex (3032, 2022-12-18)
paper/isabelle.sty (8434, 2022-12-18)
paper/isabelle.tex (8384, 2022-12-18)
paper/isabellesym.sty (20098, 2022-12-18)
paper/isabelletags.sty (1, 2022-12-18)
paper/network.tex (27216, 2022-12-18)
paper/oopsla.tex (22722, 2022-12-18)
paper/proof-strategy.tex (4742, 2022-12-18)
paper/proof-structure.tex (2480, 2022-12-18)
paper/references.bib (43046, 2022-12-18)
paper/relwork.tex (11481, 2022-12-18)
paper/rga-example.tex (4117, 2022-12-18)
paper/rga.tex (22363, 2022-12-18)
paper/round2.tex (2554, 2022-12-18)
paper/simple-crdts.tex (18065, 2022-12-18)
paper/splash-reviews.txt (8652, 2022-12-18)
src/ (0, 2022-12-18)
src/AFP/ (0, 2022-12-18)
src/AFP/Convergence.thy (18409, 2022-12-18)
src/AFP/Counter.thy (2019, 2022-12-18)
src/AFP/Network.thy (27525, 2022-12-18)
src/AFP/ORSet.thy (10727, 2022-12-18)
src/AFP/Ordered_List.thy (12361, 2022-12-18)
src/AFP/RGA.thy (23411, 2022-12-18)
src/AFP/ROOT (330, 2022-12-18)
src/AFP/Util.thy (6057, 2022-12-18)
src/AFP/document/ (0, 2022-12-18)
src/AFP/document/root.bib (34519, 2022-12-18)
... ...
Isabelle formalisation of CRDTs
===============================
This repository shows how to use [Isabelle](http://isabelle.in.tum.de/)
(theorem-proving software) to prove the correctness of several operation-based
[CRDTs](https://hal.inria.fr/inria-00555588) (data structures that can be edited
concurrently and merged automatically).
The results from this work were published in a paper titled
[Verifying strong eventual consistency in distributed systems](https://dl.acm.org/citation.cfm?doid=3152284.3133933)
at OOPSLA 2017 ([arXiv version](https://arxiv.org/abs/1707.01747)). Please cite it as:
> Victor B. F. Gomes, Martin Kleppmann, Dominic P. Mulligan, and Alastair R. Beresford.
> Verifying Strong Eventual Consistency in Distributed Systems.
> Proceedings of the ACM on Programming Languages (PACMPL), Vol. 1, Issue OOPSLA, October 2017.
> [doi:10.1145/3133933](https://doi.org/10.1145/3133933)
The formal proof development is published in the
[Isabelle Archive of Formal Proofs](https://www.isa-afp.org/index.html) under the title
[A framework for establishing Strong Eventual Consistency for Conflict-free Replicated Datatypes](https://www.isa-afp.org/entries/CRDT.html) (July 2017).
About
-----
This project was developed by
[Victor Gomes](http://www.cl.cam.ac.uk/~vb358/),
[Martin Kleppmann](http://martin.kleppmann.com/),
[Dominic Mulligan](http://dominic-mulligan.co.uk/), and
[Alastair Beresford](http://www.cl.cam.ac.uk/~arb33/).
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.
近期下载者：
相关文件：
收藏者：