Véronique Benzaken, Evelyne Contejean, Mohammed Houssem Hachmaoui, Chantal Keller, Louis Mandel, Avraham Shinnar, Jérôme Siméon. Translating canonical SQL to imperative code in Coq. Proceedings of the ACM on Programming Languages, 6(OOPSLA):1-27, 2022. [doi]
Abstract is missing.