A Coq mechanised formal semantics for realistic SQL queries - formally reconciling SQL and bag relational algebra
CPP '19: 8th ACM SIGPLAN International Conference on Certified Programs and Proofs Cascais Portugal January, 2019, pp. 249-261, 2019.
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 further pro...More
Full Text (Upload PDF)
PPT (Upload PPT)