Coq 中的向量时钟：一份经验报告
分布式、并行与集群计算
2014-06-18 v1 编程语言
软件工程
摘要
本报告记录了在 Coq 证明助手中实现向量时钟的过程，以便将其提取并用于受 Dynamo 启发的分布式数据存储 Riak 中。在本报告中，我们关注的是将在证明助手中提取的 Core Erlang 代码用于生产级 Erlang 应用程序时所面临的技术挑战，而非模型本身的验证。
引用
@article{arxiv.1406.4291,
title = {Vector Clocks in Coq: An Experience Report},
author = {Christopher Meiklejohn},
journal= {arXiv preprint arXiv:1406.4291},
year = {2014}
}