Maintaining Database Integrity with Refinement Types
Given recent advances in automated theorem proving, the authors present a new method for determining whether database transactions preserve integrity constraints. They consider check constraints and referential-integrity constraints - extracted from SQL table declarations - and application-level invariants expressed as formulas of first-order logic. The motivation is to use static analysis of database transactions at development time, to catch bugs early, or during deployment, to allow only integrity-preserving stored procedures to be accepted. They work in the setting of a functional multi-tier language, where functional code is compiled to SQL that queries and updates a relational database.