Translating canonical SQL to imperative code in Coq
summary
A mechanically verified compiler named DBCert translates a canonical SQL subset with correlated queries and NULL semantics into an imperative language using Coq proofs; it first lowers SQL to a Nested Relational Algebra, runs certified query optimizations, then converts via the Nested Relational Calculus into an Imperative Imp that can target runtimes. The implementation produces executable JavaScript backend code (backend not certified) and shows the translation and proofs are mechanized and sufficiently efficient for preliminary experiments.
AI-written summary · about
chapters (7)
- 0:00Certified SQL compiler intro
- 1:07SQL semantics and nulls
- 4:25Compiler pipeline example
- 8:43SQL algebra to nested algebra
- 12:21Nested algebra to imperative code
- 14:49Compiler challenges and future work
- 15:53Q&A
related talks
21mGenerating Collection Transformations from Proofs
32mBecause SQL is everywhere but you don't want to use it
41mHow types can turn a SQL interpreter into a SQL compiler
20mVeriEQL: Bounded Equivalence Verification for Complex SQL Queries with Integrity(…)
35mComprehending queries over finite maps
15mWhat If Writing SQL Became Cool Again?
20mGraphiti: Bridging Graph and Relational Database Queries
13mWriting an Interpreter in SQL for Fun and No Profit!