Prosecco Seminar - Toward a Coq-verified SQL compiler
- Date : 13/02/2019
- Place : Inria de Paris, Salle JLL1
- Guest(s) : Véronique Benzaken
- Organiser(s) : Project Team Prosecco
Toward a Coq-verified SQL compiler
Véronique Benzaken, LRI - Université Paris Sud
In this talk we present ongoing work on the definition of a Coq-verified SQL complier. SQL's compilation proceeds in three main steps: syntactic analysis, semantic analysis and optimisation. This last step mixes two inter-related further phases: logical and physical optimisation, which at the end provide an execution strategy for the query. In this talk we focus on semantic analysis and optimisation. We present a Coq mechanised, executable, formal semantic for the realistic fragment of SQL consisting of select-from-where-group-by-having, nested and correlated, queries, in presence of Null values. We relate it to relational algebra so as to recover well-known, widely used in practice, logical optimisations. We last present our Coq specification and implementation of physical optimisation. We draw ways of relating system-produced evaluation strategies to their expected original semantics.