Mechanical Formalisation of Nested Relational Calculus Query Syntax and Semantics - OLIVIA WESTON (2024)
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 eﬀective 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.