Translating canonical SQL to imperative code in CoqVéronique BenzakenÉvelyne Contejeanet al.2022Proceedings of the ACM on Programming Languages