Conference Paper/Proceeding/Abstract 755 views
Prawf: An Interactive Proof System for Program Extraction
,
Olga Petrovska,
Hideki Tsuiki
Lecture Notes in Computer Science, Volume: 12098, Pages: 137 - 148
Swansea University Author:
Ulrich Berger
Full text not available from this repository: check for access using links below.
DOI (Published version): 10.1007/978-3-030-51466-2_12
Abstract
We present an interactive proof system dedicated to program extraction from proofs. In a previous paper the underlying theory IFP (Intuitionistic Fixed Point Logic) was presented and its soundnessproven. The present contribution describes a prototype implementation and explains its use through sever...
| Published in: | Lecture Notes in Computer Science |
|---|---|
| ISSN: | 0302-9743 1611-3349 |
| Published: |
Cham
Springer International Publishing
2020
|
| Online Access: |
Check full text
|
| URI: | https://cronfa.swan.ac.uk/Record/cronfa57995 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Abstract: |
We present an interactive proof system dedicated to program extraction from proofs. In a previous paper the underlying theory IFP (Intuitionistic Fixed Point Logic) was presented and its soundnessproven. The present contribution describes a prototype implementation and explains its use through several case studies. The system benefits from an improvement of the theory which makes it possible to extract programs from proofs using unrestricted strictly positive inductive and coinductive definitions, thus removing the previous admissibility restrictions. |
|---|---|
| College: |
Faculty of Science and Engineering |
| Start Page: |
137 |
| End Page: |
148 |