Download PDFOpen PDF in browser

A Coq mechanised formal semantics for realistic SQL queries : Formally reconciling SQL and (extended) relational algebra.

EasyChair Preprint no. 472

12 pagesDate: August 30, 2018

Abstract

In this article, 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, quantifiers 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 extraction mechanism to Ocaml, a Coq certified semantic analyser for a SQL compiler.

Keyphrases: Coq, Mechanised semantics, SQL

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
@Booklet{EasyChair:472,
  author = {Véronique Benzaken and Évelyne Contejean},
  title = {A Coq mechanised formal semantics for realistic SQL queries : Formally reconciling SQL and (extended) relational algebra.},
  howpublished = {EasyChair Preprint no. 472},
  doi = {10.29007/dzdg},
  year = {EasyChair, 2018}}
Download PDFOpen PDF in browser