No Cover Image

Journal article 1123 views

From coinductive proofs to exact real arithmetic: theory and applications

Ulrich Berger Orcid Logo, Reinhard Kahle

Logical Methods in Computer Science, Volume: 7, Issue: 1

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.2168/LMCS-7(1:8)2011

Abstract

<p>Based on a new coinductive characterization of continuous functions we extract certified programs for exact real number computation from constructive proofs. The extracted programs construct and combine exact real number algorithms with respect to the binary signed digit representation of r...

Full description

Published in: Logical Methods in Computer Science
ISSN: 1860-5974
Published: 2011
Online Access: Check full text

URI: https://cronfa.swan.ac.uk/Record/cronfa5271
Tags: Add Tag
No Tags, Be the first to tag this record!
first_indexed 2013-07-23T11:52:09Z
last_indexed 2018-02-09T04:31:26Z
id cronfa5271
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2013-10-17T11:59:38.3208965</datestamp><bib-version>v2</bib-version><id>5271</id><entry>2011-10-01</entry><title>From coinductive proofs to exact real arithmetic: theory and applications</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>2011-10-01</date><deptcode>SCS</deptcode><abstract>&lt;p&gt;Based on a new coinductive characterization of continuous functions we extract certified programs for exact real number computation from constructive proofs. The extracted programs construct and combine exact real number algorithms with respect to the binary signed digit representation of real numbers. The data type corresponding to the coinductive definition of continuous functions consists of finitely branching non-wellfounded trees describing when the algorithm writes and reads digits. We discuss several examples including the extraction of programs for polynomials up to degree two and the definite integral of continuous maps.&lt;/p&gt;</abstract><type>Journal Article</type><journal>Logical Methods in Computer Science</journal><volume>7</volume><journalNumber>1</journalNumber><paginationStart/><paginationEnd/><publisher/><placeOfPublication/><issnPrint>1860-5974</issnPrint><issnElectronic/><keywords/><publishedDay>31</publishedDay><publishedMonth>12</publishedMonth><publishedYear>2011</publishedYear><publishedDate>2011-12-31</publishedDate><doi>10.2168/LMCS-7(1:8)2011</doi><url/><notes/><college>COLLEGE NANME</college><department>Computer Science</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>SCS</DepartmentCode><institution>Swansea University</institution><apcterm/><lastEdited>2013-10-17T11:59:38.3208965</lastEdited><Created>2011-10-01T00:00:00.0000000</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>Reinhard</firstname><surname>Kahle</surname><order>2</order></author></authors><documents/><OutputDurs/></rfc1807>
spelling 2013-10-17T11:59:38.3208965 v2 5271 2011-10-01 From coinductive proofs to exact real arithmetic: theory and applications 61199ae25042a5e629c5398c4a40a4f5 0000-0002-7677-3582 Ulrich Berger Ulrich Berger true false 2011-10-01 SCS <p>Based on a new coinductive characterization of continuous functions we extract certified programs for exact real number computation from constructive proofs. The extracted programs construct and combine exact real number algorithms with respect to the binary signed digit representation of real numbers. The data type corresponding to the coinductive definition of continuous functions consists of finitely branching non-wellfounded trees describing when the algorithm writes and reads digits. We discuss several examples including the extraction of programs for polynomials up to degree two and the definite integral of continuous maps.</p> Journal Article Logical Methods in Computer Science 7 1 1860-5974 31 12 2011 2011-12-31 10.2168/LMCS-7(1:8)2011 COLLEGE NANME Computer Science COLLEGE CODE SCS Swansea University 2013-10-17T11:59:38.3208965 2011-10-01T00:00:00.0000000 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Ulrich Berger 0000-0002-7677-3582 1 Reinhard Kahle 2
title From coinductive proofs to exact real arithmetic: theory and applications
spellingShingle From coinductive proofs to exact real arithmetic: theory and applications
Ulrich Berger
title_short From coinductive proofs to exact real arithmetic: theory and applications
title_full From coinductive proofs to exact real arithmetic: theory and applications
title_fullStr From coinductive proofs to exact real arithmetic: theory and applications
title_full_unstemmed From coinductive proofs to exact real arithmetic: theory and applications
title_sort From coinductive proofs to exact real arithmetic: theory and applications
author_id_str_mv 61199ae25042a5e629c5398c4a40a4f5
author_id_fullname_str_mv 61199ae25042a5e629c5398c4a40a4f5_***_Ulrich Berger
author Ulrich Berger
author2 Ulrich Berger
Reinhard Kahle
format Journal article
container_title Logical Methods in Computer Science
container_volume 7
container_issue 1
publishDate 2011
institution Swansea University
issn 1860-5974
doi_str_mv 10.2168/LMCS-7(1:8)2011
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 <p>Based on a new coinductive characterization of continuous functions we extract certified programs for exact real number computation from constructive proofs. The extracted programs construct and combine exact real number algorithms with respect to the binary signed digit representation of real numbers. The data type corresponding to the coinductive definition of continuous functions consists of finitely branching non-wellfounded trees describing when the algorithm writes and reads digits. We discuss several examples including the extraction of programs for polynomials up to degree two and the definite integral of continuous maps.</p>
published_date 2011-12-31T03:06:19Z
_version_ 1763749689176358912
score 11.035634

Similar Items