A Formalization of SQL with Nulls

Area of Science:

• Computer Science
• Formal Methods
• Database Systems

Background:

• SQL is the dominant declarative language, but its standard relies on ambiguous natural language, leading to implementation variations.
• Existing formal semantics for SQL often omit crucial features like null values, set/bag operations, and lateral joins.
• The lack of a formal semantics hinders the validation of database implementation soundness and query equivalence.

Purpose of the Study:

• To mechanize a formal semantics for SQL that encompasses set/bag operations, lateral joins, nested subqueries, and null values.
• To validate key metatheoretic properties of the formalized SQL semantics.
• To formalize a flat relational calculus with null values and demonstrate its translation into SQL.

Main Methods:

• Utilized the Coq proof assistant for mechanizing the formal semantics of SQL.
• Developed a formal semantics supporting advanced SQL features including null values.
• Formalized a relational calculus and proved a certified translation to SQL.

Main Results:

• Successfully mechanized a comprehensive formal semantics for SQL in Coq.
• Validated critical metatheoretic properties of the formalized semantics.
• Established a certified translation from a relational calculus with null values to SQL.

Conclusions:

• The mechanization provides a foundation for validating SQL implementations and understanding query behavior with null values.
• This work addresses a long-standing challenge in formalizing the full SQL standard.
• The framework enables formal reasoning about database queries and translations.