Q^∗cert: A platform for implementing and verifying query compilers

We present Q∗cert, a platform for the specification, verification, and implementation of query compilers written using the Coq proof assistant. The Q∗cert platform is open source and includes some support for SQL and OQL, and for code generation to Spark and Cloudant. It internally relies on familiar database intermediate representations, notably the nested relational algebra and calculus and a novel extension of the nested relational algebra that eases the handling of environments. The platform also comes with simple but functional and extensible query optimizers. We demonstrate how the platform can be used to implement a compiler for a new input language or develop new optimizations that can be formally verified. We also demonstrate a web-based interface that allows the developer to explore various compilation and optimization strategies.