论文标题
COQ平台可靠地重现了机器检查的证明
Reliably Reproducing Machine-Checked Proofs with the Coq Platform
论文作者
论文摘要
COQ平台是COQ证明助手的连续开发分布，以及常用的库，插件和外部工具，可用于基于COQ的正式验证项目。 COQ平台可以在研究，教育和行业中复制和扩展COQ工件，例如正式的数学和经过验证的软件系统。在本文中，我们描述了平台的背景和动力，并概述了其组织和发展过程。我们还将COQ平台与证明助理社区（例如Isabelle and Lean）以及更广泛的开源软件社区中的类似分布和流程进行了比较。
The Coq Platform is a continuously developed distribution of the Coq proof assistant together with commonly used libraries, plugins, and external tools useful in Coq-based formal verification projects. The Coq Platform enables reproducing and extending Coq artifacts in research, education, and industry, e.g., formalized mathematics and verified software systems. In this paper, we describe the background and motivation for the Platform, and outline its organization and development process. We also compare the Coq Platform to similar distributions and processes in the proof assistant community, such as for Isabelle and Lean, and in the wider open source software community.
