Write a Blog >>
Tue 20 Jun 2017 14:50 - 15:15 at Aula Master - Functional Programming and Correctness Chair(s): Francesco Logozzo

Every database system contains a query optimizer that performs query rewrites. Unfortunately, developing query optimizers remains a highly challenging task. Part of the challenges comes from the intricacies and rich features of query languages, which makes reasoning about rewrite rules difficult. In this paper, we propose a machine-checkable denotational semantics for SQL, the de facto language for relational database, for rigorously validating rewrite rules. Unlike previously proposed semantics that are either non-mechanized or only cover a small amount of SQL language features, our semantics covers all major features of SQL, including bags, correlated subqueries, aggregation, and indexes. Our mechanized semantics, called HoTT SQL, is based on K-Relations and homotopy type theory, where we denote relations as mathematical functions from tuples to univalent types. We have implemented HoTTSQL in Coq, which takes only fewer than 300 lines of code and have proved a wide range of SQL rewrite rules, including those from database research literature (e.g., magic set rewrites) and real-world query optimizers (e.g., subquery elimination). Several of these rewrite rules have never been previously proven correct. In addition, while query equivalence is generally undecidable, we have implemented an automated decision procedure using HoTTSQL for conjunctive queries: a well studied decidable fragment of SQL that encompasses many real-world queries.

Tue 20 Jun

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

14:00 - 15:40
Functional Programming and CorrectnessPLDI Research Papers at Aula Master
Chair(s): Francesco Logozzo Facebook
14:00
25m
Talk
Compiling without continuations
PLDI Research Papers
Luke Maurer University of Oregon, USA, Paul Downen University of Oregon, USA, Zena M. Ariola University of Oregon, USA, Simon Peyton Jones Microsoft Research, Cambridge
Media Attached
14:25
25m
Talk
FunTAL: Reasonably Mixing a Functional Language with Assembly
PLDI Research Papers
Daniel Patterson Northeastern University, Jamie Perconti Northeastern University, Christos Dimoulas Harvard University, USA, Amal Ahmed Northeastern University, USA
Media Attached
14:50
25m
Talk
HoTTSQL: Proving Query Rewrites with Univalent SQL Semantics
PLDI Research Papers
Shumo Chu University of Washington, USA, Konstantin Weitz University of Washington, USA, Alvin Cheung University of Washington, Dan Suciu University of Washington
Media Attached
15:15
25m
Talk
Levity Polymorphism
PLDI Research Papers
Richard A. Eisenberg Bryn Mawr College, USA, Simon Peyton Jones Microsoft Research, Cambridge
Media Attached