用Coq平台可靠地复制机读校样
Reliably Reproducing Machine-Checked Proofs with the Coq Platform
摘要：
Coq Platform是Coq证明助手的一个不断开发的发行版，它与常用的库、插件和外部工具一起，在基于Coq的形式化验证项目中非常有用。Coq平台能够在研究、教育和工业中再现和扩展Coq工件，例如，形式化的数学和经过验证的软件系统。在本文中，我们描述了该平台的背景和动机，并概述了其组织和发展过程。我们还将Coq平台与证明助手社区中的类似发行版和流程进行了比较，例如Isabelle和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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
