Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Tue 15 Jan 2019 14:30 - 15:00 at Sala XII - Research Papers: Program Verification Chair(s): Nicolas Tabareau

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
Times are displayed in time zone: (GMT+01:00) Greenwich Mean Time : Belfast change

14:00 - 15:30: CPP 2019 - Research Papers: Program Verification at Sala XII
Chair(s): Nicolas TabareauInria
CPP-201914:00 - 14:30
Research paper
Qianchuan YePurdue University, Benjamin DelawarePurdue University
CPP-201914:30 - 15:00
Research paper
Véronique BenzakenLRI, Université Paris-Sud, Evelyne Contejean
CPP-201915:00 - 15:30
Research paper
Susannah Mansky, Elsa GunterUniversity of Illinois