一句话：报告用 Coq 证明助手原型化查询编译器并移植到 Java 的工业经验与利弊。
本文是一篇经验报告，关注工业项目中如何利用函数式编程与形式验证工具快速原型化新特性，同时应对与现有产品代码集成及技术转移的挑战。作者将 Coq 证明助手用作构建查询编译器的原型环境，该编译器面向 IBM 的 ODM Insights 产品。文章讨论了使用 Coq 进行此类原型开发的优点与不足，并描述了为满足产品集成需求而将编译器移植到 Java 的方法论。
Designing and prototyping new features is important in many industrial projects. Functional programming and formal verification tools can prove valuable for that purpose, but lead to challenges when integrating with existing product code or when planning technology transfer. This article reports on our experience using the Coq proof assistant as a prototyping environment for building a query compiler intended for use in IBM's ODM Insights product. We discuss the pros and cons of using Coq for this purpose and describe our methodology for porting the compiler to Java, as required for product integration.
@article{AuerbachHMSS17,
title = {Prototyping a query compiler using Coq (experience report)},
author = {Joshua S. Auerbach and Martin Hirzel and Louis Mandel and Avraham Shinnar and Jérôme Siméon},
journal = {Proceedings of the ACM on Programming Languages},
volume = {1},
number = {ICFP},
year = {2017},
doi = {10.1145/3110253}
}