Project: Programming Database Theory: Using a theorem prover to formalize database theory
Description
Proving a theorem is similar to programming: in both cases the solution is a sequence of precise instructions to obtain the output/theorem given the input/assumptions. In fact, there are programming languages such as Lean, Coq, and Isabelle that can be used to prove theorems. Lean [1] is both an open source theorem prover and general purpose functional programming language developed by Microsoft that is rapidly gaining popularity because of its user friendliness and its mature and coherent math library. Currently, no database theory has been implemented in Lean.
In this project, you would create a first implementation of some basic database theory in Lean. The impact of this project can be significant as such an implementation will likely be adopted by others in the near future and may become part of a standard Lean library. Inspiration can be taken from [2], where some basic database theory is implemented in Coq, with its source code freely available. Alternatively, it is also possible in this project to extend the Coq implementation with additional theorems, like normal forms.
[1] Microsoft Lean Theorem Prover. https://leanprover.github.io/
[2] V. Benzaken, E. Contejean and S. Dumbrava: A Coq Formalization of the Relational Data Model, Proceedings of the 23rd European Symposium on Programming (ESOP 2014), doi:10.1007/978-3-642-54833-8_11. https://www.lri.fr/~benzaken/papers/esop14.pdf, source code at https://web.archive.org/web/20150915065725/http://datacert.lri.fr/esop/html/Datacert.AdditionalMaterial.html
Details
- Supervisor
-
Robert Brijder
- Interested?
- Get in contact