No Cover Image

Conference Paper/Proceeding/Abstract 755 views

Prawf: An Interactive Proof System for Program Extraction

Ulrich Berger Orcid Logo, Olga Petrovska, Hideki Tsuiki

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

Swansea University Author: 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
Tags: Add Tag
No Tags, Be the first to tag this record!
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>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>SCS</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>Computer Science</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>SCS</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>Ulrich</firstname><surname>Berger</surname><orcid>0000-0002-7677-3582</orcid><order>1</order></author><author><firstname>Olga</firstname><surname>Petrovska</surname><order>2</order></author><author><firstname>Hideki</firstname><surname>Tsuiki</surname><order>3</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 61199ae25042a5e629c5398c4a40a4f5 0000-0002-7677-3582 Ulrich Berger Ulrich Berger true false 2021-09-20 SCS 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 Computer Science COLLEGE CODE SCS 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 Ulrich Berger 0000-0002-7677-3582 1 Olga Petrovska 2 Hideki Tsuiki 3
title Prawf: An Interactive Proof System for Program Extraction
spellingShingle Prawf: An Interactive Proof System for Program Extraction
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 61199ae25042a5e629c5398c4a40a4f5
author_id_fullname_str_mv 61199ae25042a5e629c5398c4a40a4f5_***_Ulrich Berger
author Ulrich Berger
author2 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-24T04:14:10Z
_version_ 1763753957897797632
score 11.037581

Similar Items