朝向可扩展的证明引擎：Coq的高效原型重写基元
摘要：扩大验证工作的规模以适应系统的复杂性和大小带来的挑战。我们提出了一个研究议程，旨在通过研究证明引擎的渐进性能和重新设计其构建模块，构建一个高性能的证明引擎。作为一个案例研究，我们探索了等式重写，并引入了一个新颖的原型证明引擎构建模块，用于Coq中的重写，利用反射证明增强性能。我们的原型实现可以显著改进验证编译器的开发，如在Fiat密码工具链的案例研究中所示。所得到的提取的命令行编译器速度快了约1000倍，同时具有更简单的编译器特定的证明。这项工作为扩大验证工作奠定了一些基础，为实现具有良好渐进性能的证明引擎做出了贡献，最终目标是实现对更大型和更复杂的系统进行验证。
作者：Jason Gross and Andres Erbsen and Jade Philipoom and Rajashree Agrawal and Adam Chlipala
论文ID：2305.02521
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-05-05