一句话：在 Coq 中机械化验证了从规范 SQL 查询到命令式代码的编译器 DBCert，覆盖相关查询与 NULL 语义。
SQL 虽广泛使用，但在相关查询与 NULL 值语义等关键特性上，许多实现存在分歧或缺陷。本文提出 DBCert：首个从规范形式 SQL 查询到命令式代码的机械化验证编译器。其贡献包括：形式化并机械化从 SQL 到嵌套关系代数（NRA）的完整翻译，以支持查询优化；定义小型命令式语言 Imp，足以表达 SQL 并可面向 JavaScript 等多种执行语言；以及以嵌套关系演算（NRC）为中间步骤，机械化从 NRA 到 Imp 的翻译。整个编译管线在 Coq 中构造并证明，从而为 SQL 查询编译提供可信基础。
SQL is by far the most widely used and implemented query language. Yet, on some key features, such as correlated queries and NULL value semantics, many implementations diverge or contain bugs. We leverage recent advances in the formalization of SQL and query compilers to develop DBCert, the first mechanically verified compiler from SQL queries written in a canonical form to imperative code. Building DBCert required several new contributions which are described in this paper. First, we specify and mechanize a complete translation from SQL to the Nested Relational Algebra which can be used for query optimization. Second, we define Imp, a small imperative language sufficient to express SQL and which can target several execution languages including JavaScript. Finally, we develop a mechanized translation from the nested relational algebra to Imp, using the nested relational calculus as an intermediate step.
@article{paperbot1529,
title = {Translating canonical SQL to imperative code in Coq},
author = {Véronique Benzaken and Évelyne Contejean and Mohammed Houssem Hachmaoui and Chantal Keller and Louis Mandel and Avraham Shinnar and Jérôme Siméon},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {OOPSLA1},
year = {2022},
doi = {10.1145/3527327}
}