A query compiler written using the Coq proof assistant
and a platform for implementing and verifying query compilers.

What is Q*cert?

Q*cert is a query compiler: it takes some input query and generates code for execution. It can compile several source query languages, such as (subsets of) SQL and OQL. It can produce code for several target backends, such as Java, JavaScript, Cloudant and Spark.

Q*cert implements several intermediate languages useful for compilation and optimization. The semantics of each of them is precisely defined using the Coq proof assistant. Using Coq allows to prove properties on these languages, to verify the correctness of the translation from one to another, and to check that optimizations are correct.

An architecture made of small and well defined components makes Q*cert a promising platform for implementing or verifying new query languages and to develop new optimizations.

Q*cert Specification

The code for the compiler is available as open-source on github.

The compiler architecture and the compilation paths are discribed in the compiler driver and can be represented by the following figure:

Compilation Paths

The supported languages are:


Additional information on some of the novel aspects of the Q*cert work can be found in research publications:

Related Projects

Applying formal verification techniques to query languages and compilers is an active research area. The following projects have close connections with our work:


Q*cert initial source code was developed at the IBM T.J. Watson Research Center by Josh Auerbach, Stefan Fehrenbach, Martin Hirzel, Louis Mandel, Avraham Shinnar and Jerome Simeon.