E-Thesis 310 views 172 downloads
Enhanced Realizability Interpretation for Program Extraction / OLGA PETROVSKA
Swansea University Author: 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 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| 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 |