Title: Proof-driven query planning

Abstract:

This talk will discuss a very general "query planning" problem. We are given as input a query Q, a set of database integrity constraints, a target "plan language" (e.g. the plan language of a database manager), and a cost metric on plans. We want to determine if there is a plan in the target language that is equivalent to Q on all inputs satisfying the constraints, and if so find such a plan  optimizing the cost metric. That is, we want to see if there is a plan that answers the query, and if there is find the best plan.

We approach this problem using a method that goes back to the 1950's, combining the use of interpolation for generating plans from proofs with proof systems for analyzing the interaction of database queries, access restrictions, and integrity constraints. The talk will give a look at the resulting system, PDQ, along with a quick tour of the underlying theory.

This includes work with Balder ten Cate, Julien Leblay, and Efi Tsamoura.

About the speaker: http://www.cs.ox.ac.uk/michael.benedikt/