Schedule - PGConf.EU 2014

Formalising SQL in Higher-Order Logic

Date: 2014-10-23
Time: 12:50–13:40
Room: Medici I
Level: Advanced

In this talk we discuss the first concrete achievements of an ongoing project which applies formal methods to the PostgreSQL query planner.

The SQL language draws its origins from the Relational Data Model, which was explicitely founded on Set Theory. It can be argued that such rigorous foundations are one of the reasons of its popularity, even after several decades.

Also, recent years have seen a big progress of computer proving technologies, which nowadays can be productively applied to critical real-world problems, such as improving database querying capabilities.

Towards this goal, we started building a system in which it is possible to transform SQL queries using computer-verified rules; as a first outcome, earlier this year the University of Florence (Italy) produced a complete formalisation of Relational Algebra within the HOL Light system.

After giving a brief account of this work, we will outline subsequent goals of the project, sketching a plan which will eventually lead to the integration with the PostgreSQL query planner.

Speaker