A Coq Mechanised Formal Semantics for Realistic SQL Queries - Formally Reconciling SQL and Bag Relational Algebra
In this article, we provide a Coq mechanised, executable, formal semantics for a realistic fragment of SQL consisting of select [distinct] from where group by having queries with NULL values, functions, aggregates, quantifiers and nested potentially correlated sub-queries. Relying on the Coq extraction mechanism to Ocaml, we produce a Coq certified semantic analyser for a SQL compiler. We then relate this fragment to a Coq formalised (extended) relational algebra that enjoys a bag semantics hence recovering all well-known algebraic equivalences upon which are based most of compilation optimisations. By doing so, we provide the first formally mechanised proof of the equivalence of SQL and extended relational algebra.
Tue 15 Jan
|14:00 - 14:30|
|14:30 - 15:00|
A Coq Mechanised Formal Semantics for Realistic SQL Queries - Formally Reconciling SQL and Bag Relational AlgebraDOI
|15:00 - 15:30|