Translating Canonical SQL to Imperative Code in Coq

Explore a groundbreaking presentation on DBCert, the first mechanically verified compiler that translates SQL queries in canonical form to imperative code. Delve into the innovative contributions made by researchers Véronique Benzaken, Évelyne Contejean, Houssem Hachmaoui, Chantal Keller, Louis Mandel, Avraham Shinnar, and Jerome Simeon. Learn about the complete translation from SQL to the Nested Relational Algebra, the development of Imp (a small imperative language for SQL targeting), and the mechanized translation process from nested relational algebra to Imp. Gain insights into how this work addresses divergences and bugs in SQL implementations, particularly in areas such as correlated queries and NULL value semantics.