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.

Cited by: 0|Bibtex|Views0|Links
EI

Abstract:

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

Code:

Data:

Your rating :
0

 

Tags
Comments