Book chapter 979 views 204 downloads
Optimized Program Extraction for Induction and Coinduction
Sailing Routes in the World of Computation, Volume: 10936, Pages: 70 - 80
Swansea University Authors:
Ulrich Berger , Olga Petrovska
-
PDF | Accepted Manuscript
Download (327.7KB)
DOI (Published version): 10.1007/978-3-319-94418-0_7
Abstract
The paper proves soundness of an optimized realizability interpretation for a logic supporting strictly positive induction and coinduction. The optimization concerns the special treatment of Harrop formulas which yields simpler extracted programs. It is shown that wellfounded induction is an instanc...
Published in: | Sailing Routes in the World of Computation |
---|---|
ISBN: | 9783319944173 9783319944180 |
ISSN: | 0302-9743 1611-3349 |
Published: |
Cham
Springer International Publishing
2018
|
Online Access: |
Check full text
|
URI: | https://cronfa.swan.ac.uk/Record/cronfa39885 |
Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
first_indexed |
2018-07-30T13:32:07Z |
---|---|
last_indexed |
2019-06-28T14:32:04Z |
id |
cronfa39885 |
recordtype |
SURis |
fullrecord |
<?xml version="1.0" encoding="utf-8"?><rfc1807 xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xsd="http://www.w3.org/2001/XMLSchema"><bib-version>v2</bib-version><id>39885</id><entry>2018-05-02</entry><title>Optimized Program Extraction for Induction and Coinduction</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><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></swanseaauthors><date>2018-05-02</date><deptcode>SCS</deptcode><abstract>The paper proves soundness of an optimized realizability interpretation for a logic supporting strictly positive induction and coinduction. The optimization concerns the special treatment of Harrop formulas which yields simpler extracted programs. It is shown that wellfounded induction is an instance of strictly positive induction and from this a new computationally meaningful formulation of the Archimedean property for real numbers is derived. An example of program extraction in computableanalysis shows that Archimedean induction can be used to eliminate countable choice</abstract><type>Book chapter</type><journal>Sailing Routes in the World of Computation</journal><volume>10936</volume><journalNumber/><paginationStart>70</paginationStart><paginationEnd>80</paginationEnd><publisher>Springer International Publishing</publisher><placeOfPublication>Cham</placeOfPublication><isbnPrint>9783319944173</isbnPrint><isbnElectronic>9783319944180</isbnElectronic><issnPrint>0302-9743</issnPrint><issnElectronic>1611-3349</issnElectronic><keywords/><publishedDay>1</publishedDay><publishedMonth>1</publishedMonth><publishedYear>2018</publishedYear><publishedDate>2018-01-01</publishedDate><doi>10.1007/978-3-319-94418-0_7</doi><url>http://dx.doi.org/10.1007/978-3-319-94418-0_7</url><notes/><college>COLLEGE NANME</college><department>Computer Science</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>SCS</DepartmentCode><institution>Swansea University</institution><apcterm/><funders/><projectreference/><lastEdited>2023-05-22T15:01:12.7002403</lastEdited><Created>2018-05-02T22:51:06.7841193</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><orcid>0000-0003-1170-8816</orcid><order>2</order></author></authors><documents><document><filename>0039885-02052018230228.pdf</filename><originalFilename>mainv3.pdf</originalFilename><uploaded>2018-05-02T23:02:28.4730000</uploaded><type>Output</type><contentLength>286337</contentLength><contentType>application/pdf</contentType><version>Accepted Manuscript</version><cronfaStatus>true</cronfaStatus><embargoDate>2019-07-03T00:00:00.0000000</embargoDate><copyrightCorrect>true</copyrightCorrect><language>eng</language></document></documents><OutputDurs/></rfc1807> |
spelling |
v2 39885 2018-05-02 Optimized Program Extraction for Induction and Coinduction 61199ae25042a5e629c5398c4a40a4f5 0000-0002-7677-3582 Ulrich Berger Ulrich Berger true false 3f0bf84d3c8d15113f3f0da0aab6b783 0000-0003-1170-8816 Olga Petrovska Olga Petrovska true false 2018-05-02 SCS The paper proves soundness of an optimized realizability interpretation for a logic supporting strictly positive induction and coinduction. The optimization concerns the special treatment of Harrop formulas which yields simpler extracted programs. It is shown that wellfounded induction is an instance of strictly positive induction and from this a new computationally meaningful formulation of the Archimedean property for real numbers is derived. An example of program extraction in computableanalysis shows that Archimedean induction can be used to eliminate countable choice Book chapter Sailing Routes in the World of Computation 10936 70 80 Springer International Publishing Cham 9783319944173 9783319944180 0302-9743 1611-3349 1 1 2018 2018-01-01 10.1007/978-3-319-94418-0_7 http://dx.doi.org/10.1007/978-3-319-94418-0_7 COLLEGE NANME Computer Science COLLEGE CODE SCS Swansea University 2023-05-22T15:01:12.7002403 2018-05-02T22:51:06.7841193 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Ulrich Berger 0000-0002-7677-3582 1 Olga Petrovska 0000-0003-1170-8816 2 0039885-02052018230228.pdf mainv3.pdf 2018-05-02T23:02:28.4730000 Output 286337 application/pdf Accepted Manuscript true 2019-07-03T00:00:00.0000000 true eng |
title |
Optimized Program Extraction for Induction and Coinduction |
spellingShingle |
Optimized Program Extraction for Induction and Coinduction Ulrich Berger Olga Petrovska |
title_short |
Optimized Program Extraction for Induction and Coinduction |
title_full |
Optimized Program Extraction for Induction and Coinduction |
title_fullStr |
Optimized Program Extraction for Induction and Coinduction |
title_full_unstemmed |
Optimized Program Extraction for Induction and Coinduction |
title_sort |
Optimized Program Extraction for Induction and Coinduction |
author_id_str_mv |
61199ae25042a5e629c5398c4a40a4f5 3f0bf84d3c8d15113f3f0da0aab6b783 |
author_id_fullname_str_mv |
61199ae25042a5e629c5398c4a40a4f5_***_Ulrich Berger 3f0bf84d3c8d15113f3f0da0aab6b783_***_Olga Petrovska |
author |
Ulrich Berger Olga Petrovska |
author2 |
Ulrich Berger Olga Petrovska |
format |
Book chapter |
container_title |
Sailing Routes in the World of Computation |
container_volume |
10936 |
container_start_page |
70 |
publishDate |
2018 |
institution |
Swansea University |
isbn |
9783319944173 9783319944180 |
issn |
0302-9743 1611-3349 |
doi_str_mv |
10.1007/978-3-319-94418-0_7 |
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 |
url |
http://dx.doi.org/10.1007/978-3-319-94418-0_7 |
document_store_str |
1 |
active_str |
0 |
description |
The paper proves soundness of an optimized realizability interpretation for a logic supporting strictly positive induction and coinduction. The optimization concerns the special treatment of Harrop formulas which yields simpler extracted programs. It is shown that wellfounded induction is an instance of strictly positive induction and from this a new computationally meaningful formulation of the Archimedean property for real numbers is derived. An example of program extraction in computableanalysis shows that Archimedean induction can be used to eliminate countable choice |
published_date |
2018-01-01T15:01:10Z |
_version_ |
1766603170523381760 |
score |
11.021648 |