uu.seUppsala University Publications
Change search
ReferencesLink to record
Permanent link

Direct link
Maintaining Database Integrity with Refinement Types
University of Cambridge.
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science. (Mobility)
Microsoft Research, Cambridge.
2011 (English)In: ECOOP 2011 – Object-Oriented Programming / [ed] Mezini, Mira, Berlin: Springer-Verlag , 2011, 484-509 p.Conference paper (Refereed)
Abstract [en]

Taking advantage of recent advances in automated theorem proving, we present a new method for determining whether database transactions preserve integrity constraints. We consider check constraints and referential-integrity constraints—extracted from SQL table declarations—and application-level in- variants expressed as formulas of first-order logic. Our 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. We work in the setting of a functional multi-tier language, where functional code is compiled to SQL that queries and updates a relational database. We use refinement types to track constraints on data and the underlying database. Our analysis uses a refinement-type checker, which relies on recent highly efficient SMT algorithms to check proof obligations. Our method is based on a list-processing semantics for an SQL fragment within the functional language, and is illustrated by a series of examples. 

Place, publisher, year, edition, pages
Berlin: Springer-Verlag , 2011. 484-509 p.
, Lecture Notes in Computer Science, 6813
National Category
Computer Science
URN: urn:nbn:se:uu:diva-162158DOI: 10.1007/978-3-642-22655-7_23ISBN: 978-3-642-22654-0OAI: oai:DiVA.org:uu-162158DiVA: diva2:459154
Available from: 2011-11-24 Created: 2011-11-24 Last updated: 2011-11-25Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full text

Search in DiVA

By author/editor
Borgström, Johannes
By organisation
Computing Science
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Altmetric score

Total: 233 hits
ReferencesLink to record
Permanent link

Direct link