Translating Canonical SQL to Imperative Code in CoqVéronique BenzakenEveleyne Contejeanet al.2022SPLASH 2022