A Coq mechanized executable formal semantics for realistic SQL queries.
This work compiles with Coq 8.15.0:
make
make install
This code is released under the terms of the Creative Common Attribution-NonCommercial-NoDerivatives 4.0 International license; see LICENSE for details.
A Coq mechanised formal semantics for realistic SQL queries: formally reconciling SQL and bag relational algebra, Benzaken, Véronique; Contejean, Évelyne, CPP - 8th ACM SIGPLAN International Conference on Certified Programs and Proofs - 2019