A Coq Formalisation of SQL's Execution Engines. - Véronique Benzaken; Evelyne Contejean; Chantal Keller; Eunice Martins (ITP, 2018)