No Cover Image

E-Thesis 457 views 206 downloads

Enhanced Realizability Interpretation for Program Extraction / Olga Petrovska; OLGA PETROVSKA

Swansea University Authors: Olga Petrovska, OLGA PETROVSKA

DOI (Published version): 10.23889/SUthesis.57831

Abstract

This thesis presents Intuitionistic Fixed Point Logic (IFP), a schema for formal systems aimed to work with program extraction from proofs. IFP in its basic form allows proof construction based on natural deduction inference rules, extended by induction and coinduction. The corresponding system RIFP...

Full description

Published: Swansea 2021
Institution: Swansea University
Degree level: Doctoral
Degree name: Ph.D
Supervisor: Berger, Ulrich
URI: https://cronfa.swan.ac.uk/Record/cronfa57831
first_indexed 2021-09-09T15:08:40Z
last_indexed 2021-09-10T03:20:38Z
id cronfa57831
recordtype RisThesis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2021-09-09T16:46:04.7156349</datestamp><bib-version>v2</bib-version><id>57831</id><entry>2021-09-09</entry><title>Enhanced Realizability Interpretation for Program Extraction</title><swanseaauthors><author><sid>3f0bf84d3c8d15113f3f0da0aab6b783</sid><ORCID>0000-0003-1170-8816</ORCID><firstname>Olga</firstname><surname>Petrovska</surname><name>Olga Petrovska</name><active>true</active><ethesisStudent>false</ethesisStudent></author><author><sid>5edcfa07b18b9f21b539e727881e7255</sid><firstname>OLGA</firstname><surname>PETROVSKA</surname><name>OLGA PETROVSKA</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2021-09-09</date><deptcode>MACS</deptcode><abstract>This thesis presents Intuitionistic Fixed Point Logic (IFP), a schema for formal systems aimed to work with program extraction from proofs. IFP in its basic form allows proof construction based on natural deduction inference rules, extended by induction and coinduction. The corresponding system RIFP (IFP with realiz-ers) enables transforming logical proofs into programs utilizing the enhanced re-alizability interpretation. The theoretical research is put into practice in PRAWF1, a Haskell-based proof assistant for program extraction.</abstract><type>E-Thesis</type><journal/><volume/><journalNumber/><paginationStart/><paginationEnd/><publisher/><placeOfPublication>Swansea</placeOfPublication><isbnPrint/><isbnElectronic/><issnPrint/><issnElectronic/><keywords>computer science, logic, program extraction, intuitionistic logic</keywords><publishedDay>9</publishedDay><publishedMonth>9</publishedMonth><publishedYear>2021</publishedYear><publishedDate>2021-09-09</publishedDate><doi>10.23889/SUthesis.57831</doi><url/><notes>ORCiD identifier https://orcid.org/0000-0003-1170-8816</notes><college>COLLEGE NANME</college><department>Mathematics and Computer Science School</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>MACS</DepartmentCode><institution>Swansea University</institution><supervisor>Berger, Ulrich</supervisor><degreelevel>Doctoral</degreelevel><degreename>Ph.D</degreename><degreesponsorsfunders>EPSRC, EPSRC Doctoral Training Grant No. 1818640</degreesponsorsfunders><apcterm/><lastEdited>2021-09-09T16:46:04.7156349</lastEdited><Created>2021-09-09T16:06:01.1028598</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>Olga</firstname><surname>Petrovska</surname><orcid>0000-0003-1170-8816</orcid><order>1</order></author><author><firstname>OLGA</firstname><surname>PETROVSKA</surname><order>2</order></author></authors><documents><document><filename>57831__20809__0d6a393dd355438ebbe4113e6e9aff2c.pdf</filename><originalFilename>Petrovska_Olga_PhD_Thesis_Final_Redacted_Signature.pdf</originalFilename><uploaded>2021-09-09T16:33:38.5771809</uploaded><type>Output</type><contentLength>856552</contentLength><contentType>application/pdf</contentType><version>E-Thesis &#x2013; open access</version><cronfaStatus>true</cronfaStatus><documentNotes>Copyright: The author, Olga Petrovska, 2021.</documentNotes><copyrightCorrect>true</copyrightCorrect><language>eng</language></document></documents><OutputDurs/></rfc1807>
spelling 2021-09-09T16:46:04.7156349 v2 57831 2021-09-09 Enhanced Realizability Interpretation for Program Extraction 3f0bf84d3c8d15113f3f0da0aab6b783 0000-0003-1170-8816 Olga Petrovska Olga Petrovska true false 5edcfa07b18b9f21b539e727881e7255 OLGA PETROVSKA OLGA PETROVSKA true false 2021-09-09 MACS This thesis presents Intuitionistic Fixed Point Logic (IFP), a schema for formal systems aimed to work with program extraction from proofs. IFP in its basic form allows proof construction based on natural deduction inference rules, extended by induction and coinduction. The corresponding system RIFP (IFP with realiz-ers) enables transforming logical proofs into programs utilizing the enhanced re-alizability interpretation. The theoretical research is put into practice in PRAWF1, a Haskell-based proof assistant for program extraction. E-Thesis Swansea computer science, logic, program extraction, intuitionistic logic 9 9 2021 2021-09-09 10.23889/SUthesis.57831 ORCiD identifier https://orcid.org/0000-0003-1170-8816 COLLEGE NANME Mathematics and Computer Science School COLLEGE CODE MACS Swansea University Berger, Ulrich Doctoral Ph.D EPSRC, EPSRC Doctoral Training Grant No. 1818640 2021-09-09T16:46:04.7156349 2021-09-09T16:06:01.1028598 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Olga Petrovska 0000-0003-1170-8816 1 OLGA PETROVSKA 2 57831__20809__0d6a393dd355438ebbe4113e6e9aff2c.pdf Petrovska_Olga_PhD_Thesis_Final_Redacted_Signature.pdf 2021-09-09T16:33:38.5771809 Output 856552 application/pdf E-Thesis – open access true Copyright: The author, Olga Petrovska, 2021. true eng
title Enhanced Realizability Interpretation for Program Extraction
spellingShingle Enhanced Realizability Interpretation for Program Extraction
Olga Petrovska
OLGA PETROVSKA
title_short Enhanced Realizability Interpretation for Program Extraction
title_full Enhanced Realizability Interpretation for Program Extraction
title_fullStr Enhanced Realizability Interpretation for Program Extraction
title_full_unstemmed Enhanced Realizability Interpretation for Program Extraction
title_sort Enhanced Realizability Interpretation for Program Extraction
author_id_str_mv 3f0bf84d3c8d15113f3f0da0aab6b783
5edcfa07b18b9f21b539e727881e7255
author_id_fullname_str_mv 3f0bf84d3c8d15113f3f0da0aab6b783_***_Olga Petrovska
5edcfa07b18b9f21b539e727881e7255_***_OLGA PETROVSKA
author Olga Petrovska
OLGA PETROVSKA
author2 Olga Petrovska
OLGA PETROVSKA
format E-Thesis
publishDate 2021
institution Swansea University
doi_str_mv 10.23889/SUthesis.57831
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 1
active_str 0
description This thesis presents Intuitionistic Fixed Point Logic (IFP), a schema for formal systems aimed to work with program extraction from proofs. IFP in its basic form allows proof construction based on natural deduction inference rules, extended by induction and coinduction. The corresponding system RIFP (IFP with realiz-ers) enables transforming logical proofs into programs utilizing the enhanced re-alizability interpretation. The theoretical research is put into practice in PRAWF1, a Haskell-based proof assistant for program extraction.
published_date 2021-09-09T20:04:51Z
_version_ 1821346618493894656
score 11.04748

Similar Items