  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.
