Sites Inria

Version française

Prosecco Seminar

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.