DBCert

A runtime and a runner for the Coq certified compiler from SQL to JavaScript.

Requirements

This work is known to compile with Node.js 10, OCaml-4.09.1, Coq-8.11.*, and JsAst-2.0.0.

Install Node.js

https://nodejs.org/en/download/releases/

Install Opam

sudo curl -sL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh > install.sh
echo | sudo sh install.sh
eval $(opam env)
opam switch create 4.09.1 || true
opam switch set 4.09.1
opam update || true

Prepare Coq dependencies

opam repo add coq-released https://coq.inria.fr/opam/released

Compilation

Have OCaml and Coq executables in your path:

opam install -y .

Examples

To compile SQL to JavaScript:

dbcert src/tests/simple/org1.sql

To compile SQL to JavaScript and link the runtime:

dbcert -link src/tests/simple/org1.sql

To run the compiled JavaScript:

node src/dbcertRun.js src/tests/simple/org1.js src/tests/simple/db1.json

License

This code is released under the Apache 2.0 license (see LICENSE for details).

Companion paper

Translating Canonical SQL to Imperative Code in Coq, Véronique Benzaken, Évelyne Contejean, Mohammed Houssem Hachmaoui, Chantal Keller, Louis Mandel, Avraham Shinnar and Jérôme Siméon, Proceedings of the ACM on Programming Languages, OOPSLA 2022.