No Cover Image

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...

Full description

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
first_indexed 2024-11-25T14:21:40Z
last_indexed 2024-11-25T14:21:40Z
id cronfa68217
recordtype RisThesis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2024-11-07T15:51:40.5577616</datestamp><bib-version>v2</bib-version><id>68217</id><entry>2024-11-07</entry><title>Mechanical Formalisation of Nested Relational Calculus Query Syntax and Semantics</title><swanseaauthors><author><sid>44647315c9bb3e9c0b951ba55299caa9</sid><firstname>OLIVIA</firstname><surname>WESTON</surname><name>OLIVIA WESTON</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2024-11-07</date><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 e&#xFB00;ective list semantics and a denotational Prop-based semantics for the language. We create examples that show the Nested Relational Calculus&#x2019;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.</abstract><type>E-Thesis</type><journal/><volume/><journalNumber/><paginationStart/><paginationEnd/><publisher/><placeOfPublication>Swansea University, Wales, UK</placeOfPublication><isbnPrint/><isbnElectronic/><issnPrint/><issnElectronic/><keywords>Programming language theory, database theory, lambda calculus, relational calculus,nested relational calculus, Coq, Rocq, mechanical formalisation</keywords><publishedDay>27</publishedDay><publishedMonth>8</publishedMonth><publishedYear>2024</publishedYear><publishedDate>2024-08-27</publishedDate><doi/><url/><notes>A selection of content is redacted or is partially redacted from this thesis to protect sensitive and personal information.</notes><college>COLLEGE NANME</college><CollegeCode>COLLEGE CODE</CollegeCode><institution>Swansea University</institution><supervisor>Pradic, C., and Pauly, A.</supervisor><degreelevel>Master of Research</degreelevel><degreename>MRes</degreename><apcterm/><funders/><projectreference/><lastEdited>2024-11-07T15:51:40.5577616</lastEdited><Created>2024-11-07T15:46:02.6649308</Created><path><level id="1">Faculty of Science and Engineering</level><level id="2">School of Mathematics and Computer Science - Computer Science</level></path><authors><author><firstname>OLIVIA</firstname><surname>WESTON</surname><order>1</order></author></authors><documents><document><filename>68217__32894__dfd98354e85d4f23b1b8405497cad2e0.pdf</filename><originalFilename>2023_Weston_O.final.68217.pdf</originalFilename><uploaded>2024-11-07T15:50:54.3998513</uploaded><type>Output</type><contentLength>416188</contentLength><contentType>application/pdf</contentType><version>E-Thesis &#x2013; open access</version><cronfaStatus>true</cronfaStatus><documentNotes>Copyright: The Author, Olivia Weston, 2023</documentNotes><copyrightCorrect>true</copyrightCorrect><language>eng</language></document></documents><OutputDurs/></rfc1807>
spelling 2024-11-07T15:51:40.5577616 v2 68217 2024-11-07 Mechanical Formalisation of Nested Relational Calculus Query Syntax and Semantics 44647315c9bb3e9c0b951ba55299caa9 OLIVIA WESTON OLIVIA WESTON true false 2024-11-07 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. E-Thesis Swansea University, Wales, UK Programming language theory, database theory, lambda calculus, relational calculus,nested relational calculus, Coq, Rocq, mechanical formalisation 27 8 2024 2024-08-27 A selection of content is redacted or is partially redacted from this thesis to protect sensitive and personal information. COLLEGE NANME COLLEGE CODE Swansea University Pradic, C., and Pauly, A. Master of Research MRes 2024-11-07T15:51:40.5577616 2024-11-07T15:46:02.6649308 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science OLIVIA WESTON 1 68217__32894__dfd98354e85d4f23b1b8405497cad2e0.pdf 2023_Weston_O.final.68217.pdf 2024-11-07T15:50:54.3998513 Output 416188 application/pdf E-Thesis – open access true Copyright: The Author, Olivia Weston, 2023 true eng
title Mechanical Formalisation of Nested Relational Calculus Query Syntax and Semantics
spellingShingle Mechanical Formalisation of Nested Relational Calculus Query Syntax and Semantics
OLIVIA WESTON
title_short Mechanical Formalisation of Nested Relational Calculus Query Syntax and Semantics
title_full Mechanical Formalisation of Nested Relational Calculus Query Syntax and Semantics
title_fullStr Mechanical Formalisation of Nested Relational Calculus Query Syntax and Semantics
title_full_unstemmed Mechanical Formalisation of Nested Relational Calculus Query Syntax and Semantics
title_sort Mechanical Formalisation of Nested Relational Calculus Query Syntax and Semantics
author_id_str_mv 44647315c9bb3e9c0b951ba55299caa9
author_id_fullname_str_mv 44647315c9bb3e9c0b951ba55299caa9_***_OLIVIA WESTON
author OLIVIA WESTON
author2 OLIVIA WESTON
format E-Thesis
publishDate 2024
institution Swansea University
college_str Faculty of Science and Engineering
hierarchytype
hierarchy_top_id facultyofscienceandengineering
hierarchy_top_title Faculty of Science and Engineering
hierarchy_parent_id facultyofscienceandengineering
hierarchy_parent_title Faculty of Science and Engineering
department_str School of Mathematics and Computer Science - Computer Science{{{_:::_}}}Faculty of Science and Engineering{{{_:::_}}}School of Mathematics and Computer Science - Computer Science
document_store_str 0
active_str 0
description 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.
published_date 2024-08-27T20:49:12Z
_version_ 1821440006098518016
score 11.047609

Similar Items