Formalizing the nested relational calculus in a proof assistant
by Cécilia Pradic| Departments | Computer Science |
|---|---|
| Description | The nested relational calculus (NRC) is a conservative extension of the relational calculus (the core of SQL) that can manipulate nested sets and relations (while a SQL query only maps a relation to another relation). The goal of this project would be formalize various basic results about NRC in a proof assistant such as Coq or Agda. Good starting goals would be to prove the conservativity result over SQL (as was the goal of e.g. https://github.com/ezrakilty/nrc-sql), that adding various features such as sum types do not increase the power of NRC or a proof of normalization. For most of these proofs, there is an underlying algorithm, and proof assistants have typically an extraction mechanism that allow to extract e.g. Haskell or OCaml code. It would be interesting to play with these using formalization of the above. |
| Preparation | There would be two main technical aspects to get familiar with: the theory behind NRC and the proof assistant. For background on NRC, the thesis of Limsoon Wong is a good resource https://repository.upenn.edu/ircs_reports/155/ For proof assistants, I would recommend getting familiar with one; I would be able to offer support for Coq during the project, and, to a slightly lesser extent, Agda. A thesis which might be worth reading with similar aims is https://www.wisnesky.net/dissertation.pdf but beware: the author considers an extension of NRC that is not conservative over SQL (so it does not subsume the goals of this project). In case you are already familiar with a proof assistant and the mechanized formalization of deep embedding of proof systems, we can consider a more ambitious project involving NRC: formalize the main result of https://arxiv.org/abs/2005.06503 (or an extension thereof) and assess the underlying algorithm. I have already some code towards this, but this would be a much more ambitious task nonetheless. |
| Project Categories | January Cohort, Theorical Computer Science |
| Project Keywords | Databases, Logic, Proofs |
| |
| Level 6 (Undergraduate Year 3) | yes |
| Level 7 (Masters) | yes |
| Level 8 (PhD) | yes |