Abstract
In this article, we propose a Coq formalization of the relational data model which underlies relational database systems. More precisely, we present and formalize the data definition part of the model including integrity constraints. We model two different query language formalisms: relational algebra and conjunctive queries. We also present logical query optimization and prove the main “database theorems”: algebraic equivalences, the homomorphism theorem and conjunctive query minimization.
This work is partially supported by ANR project Typex no 11BS0200702.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abiteboul, S., Hull, R., Vianu, V.: Foundations of Databases. Addison-Wesley (1995)
Benzaken, V., Contejean, E., Dumbrava, S.: A Relational Library (2013), http://datacert.lri.fr/esop/html/Datacert.AdditionalMaterial.html
Chlipala, A., Malecha, J.G., Morrisett, G., Shinnar, A., Wisnesky, R.: Effective interactive proofs for higher-order imperative programs. In: Hutton, G., Tolmach, A.P. (eds.) ICFP, pp. 79–90. ACM (2009)
Filliâtre, J.-C., Paskevich, A.: Why3 - where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125–128. Springer, Heidelberg (2013)
Gonzalia, C.: Relations in Dependent Type Theory. Ph.D. thesis, Chalmers Göteborg University (2006)
Gonzalia, C.: Towards a formalisation of relational database theory in constructive type theory. In: Berghammer, R., Möller, B., Struth, G. (eds.) RelMiCS 2003. LNCS, vol. 3051, pp. 137–148. Springer, Heidelberg (2004)
Letouzey, P.: A library for finite sets
Malecha, G., Morrisett, G., Shinnar, A., Wisnesky, R.: Toward a verified relational database management system. In: ACM Int. Conf. POPL (2010)
Ramakrishnan, R., Gehrke, J.: Database management systems, 3rd edn. McGraw-Hill (2003)
The Coq Development Team: The Coq Proof Assistant Reference Manual (2010), http://coq.inria.fr , http://coq.inria.fr
Ullman, J.D.: Principles of Database Systems, 2nd edn. Computer Science Press (1982)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Benzaken, V., Contejean, É., Dumbrava, S. (2014). A Coq Formalization of the Relational Data Model. In: Shao, Z. (eds) Programming Languages and Systems. ESOP 2014. Lecture Notes in Computer Science, vol 8410. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-54833-8_11
Download citation
DOI: https://doi.org/10.1007/978-3-642-54833-8_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-54832-1
Online ISBN: 978-3-642-54833-8
eBook Packages: Computer ScienceComputer Science (R0)