No Cover Image

Conference Paper/Proceeding/Abstract 757 views

Prawf: An Interactive Proof System for Program Extraction

Olga Petrovska Orcid Logo, Ulrich Berger Orcid Logo, Olga Petrovska, Hideki Tsuiki

Lecture Notes in Computer Science, Volume: 12098, Pages: 137 - 148

Swansea University Authors: Olga Petrovska Orcid Logo, Ulrich Berger Orcid Logo

Full text not available from this repository: check for access using links below.

Check full text

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

Full description

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
first_indexed 2021-09-21T08:28:53Z
last_indexed 2021-10-15T03:23:57Z
id cronfa57995
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2021-10-14T16:56:08.6973020</datestamp><bib-version>v2</bib-version><id>57995</id><entry>2021-09-20</entry><title>Prawf: An Interactive Proof System 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>61199ae25042a5e629c5398c4a40a4f5</sid><ORCID>0000-0002-7677-3582</ORCID><firstname>Ulrich</firstname><surname>Berger</surname><name>Ulrich Berger</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2021-09-20</date><deptcode>MACS</deptcode><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.</abstract><type>Conference Paper/Proceeding/Abstract</type><journal>Lecture Notes in Computer Science</journal><volume>12098</volume><journalNumber/><paginationStart>137</paginationStart><paginationEnd>148</paginationEnd><publisher>Springer International Publishing</publisher><placeOfPublication>Cham</placeOfPublication><isbnPrint/><isbnElectronic/><issnPrint>0302-9743</issnPrint><issnElectronic>1611-3349</issnElectronic><keywords/><publishedDay>24</publishedDay><publishedMonth>6</publishedMonth><publishedYear>2020</publishedYear><publishedDate>2020-06-24</publishedDate><doi>10.1007/978-3-030-51466-2_12</doi><url/><notes/><college>COLLEGE NANME</college><department>Mathematics and Computer Science School</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>MACS</DepartmentCode><institution>Swansea University</institution><apcterm/><lastEdited>2021-10-14T16:56:08.6973020</lastEdited><Created>2021-09-20T22:52:20.0472418</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>Ulrich</firstname><surname>Berger</surname><orcid>0000-0002-7677-3582</orcid><order>2</order></author><author><firstname>Olga</firstname><surname>Petrovska</surname><order>3</order></author><author><firstname>Hideki</firstname><surname>Tsuiki</surname><order>4</order></author></authors><documents/><OutputDurs/></rfc1807>
spelling 2021-10-14T16:56:08.6973020 v2 57995 2021-09-20 Prawf: An Interactive Proof System for Program Extraction 3f0bf84d3c8d15113f3f0da0aab6b783 0000-0003-1170-8816 Olga Petrovska Olga Petrovska true false 61199ae25042a5e629c5398c4a40a4f5 0000-0002-7677-3582 Ulrich Berger Ulrich Berger true false 2021-09-20 MACS 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. Conference Paper/Proceeding/Abstract Lecture Notes in Computer Science 12098 137 148 Springer International Publishing Cham 0302-9743 1611-3349 24 6 2020 2020-06-24 10.1007/978-3-030-51466-2_12 COLLEGE NANME Mathematics and Computer Science School COLLEGE CODE MACS Swansea University 2021-10-14T16:56:08.6973020 2021-09-20T22:52:20.0472418 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Olga Petrovska 0000-0003-1170-8816 1 Ulrich Berger 0000-0002-7677-3582 2 Olga Petrovska 3 Hideki Tsuiki 4
title Prawf: An Interactive Proof System for Program Extraction
spellingShingle Prawf: An Interactive Proof System for Program Extraction
Olga Petrovska
Ulrich Berger
title_short Prawf: An Interactive Proof System for Program Extraction
title_full Prawf: An Interactive Proof System for Program Extraction
title_fullStr Prawf: An Interactive Proof System for Program Extraction
title_full_unstemmed Prawf: An Interactive Proof System for Program Extraction
title_sort Prawf: An Interactive Proof System for Program Extraction
author_id_str_mv 3f0bf84d3c8d15113f3f0da0aab6b783
61199ae25042a5e629c5398c4a40a4f5
author_id_fullname_str_mv 3f0bf84d3c8d15113f3f0da0aab6b783_***_Olga Petrovska
61199ae25042a5e629c5398c4a40a4f5_***_Ulrich Berger
author Olga Petrovska
Ulrich Berger
author2 Olga Petrovska
Ulrich Berger
Olga Petrovska
Hideki Tsuiki
format Conference Paper/Proceeding/Abstract
container_title Lecture Notes in Computer Science
container_volume 12098
container_start_page 137
publishDate 2020
institution Swansea University
issn 0302-9743
1611-3349
doi_str_mv 10.1007/978-3-030-51466-2_12
publisher Springer International Publishing
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 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.
published_date 2020-06-24T20:05:22Z
_version_ 1821346651253506048
score 11.04748

Similar Items