E-Thesis 7 views
Mechanical Formalisation of Nested Relational Calculus Query Syntax and Semantics / OLIVIA WESTON
Swansea University Author: OLIVIA WESTON
Abstract
Building on top of existing work by Wong, we exhibit an implementation of the Nested Relational Calculus of Buneman et al. in the Coq interactive theorem prover. We provide a syntax for the language. Additionally, we provide a denotational effective list semantics and a denotational Prop-based semant...
| Published: |
Swansea University, Wales, UK
2024
|
|---|---|
| Institution: | Swansea University |
| Degree level: | Master of Research |
| Degree name: | MRes |
| Supervisor: | Pradic, C., and Pauly, A. |
| URI: | https://cronfa.swan.ac.uk/Record/cronfa68217 |
| Abstract: |
Building on top of existing work by Wong, we exhibit an implementation of the Nested Relational Calculus of Buneman et al. in the Coq interactive theorem prover. We provide a syntax for the language. Additionally, we provide a denotational effective list semantics and a denotational Prop-based semantics for the language. We create examples that show the Nested Relational Calculus’capabilities as a declarative programming language. We provide a discussion on works similar to ours, justifying our design decisions. We leave the reader with multiple directions in which the project can be taken, and the expected results. |
|---|---|
| Item Description: |
A selection of content is redacted or is partially redacted from this thesis to protect sensitive and personal information. |
| Keywords: |
Programming language theory, database theory, lambda calculus, relational calculus,nested relational calculus, Coq, Rocq, mechanical formalisation |
| College: |
Faculty of Science and Engineering |