A Coq mechanised formal semantics for realistic SQL queries: formally reconciling SQL and bag relational algebra

VĂ©ronique Benzaken, Evelyne Contejean. A Coq mechanised formal semantics for realistic SQL queries: formally reconciling SQL and bag relational algebra. In Assia Mahboubi, Magnus O. Myreen, editors, Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019. pages 249-261, ACM, 2019. [doi]