E-Thesis 456 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...
| Published: |
Swansea
2021
|
|---|---|
| Institution: | Swansea University |
| Degree level: | Doctoral |
| Degree name: | Ph.D |
| Supervisor: | Berger, Ulrich |
| URI: | https://cronfa.swan.ac.uk/Record/cronfa57831 |
| 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. |
|---|---|
| Item Description: |
ORCiD identifier https://orcid.org/0000-0003-1170-8816 |
| Keywords: |
computer science, logic, program extraction, intuitionistic logic |
| College: |
Faculty of Science and Engineering |