In this talk, we provide a Coq mechanised, executable,
formal semantics for realistic SQL queries consisting
of select [distinct] from where group by having
queries with NULL values, functions, aggregates, quanti-
fiers and nested, potentially correlated, sub-queries. We
then relate this fragment to a Coq formalised (extended)
relational algebra that enjoys a bag semantics. Doing
so we provide the first formally mechanised proof of the
equivalence of SQL and extended relational algebra and,
from a compilation perspective, thanks to the Coq ex-
traction mechanism to Ocaml, a Coq certified semantic
analyser for a SQL compiler