No Cover Image

Journal article 1181 views

From coinductive proofs to exact real arithmetic: theory and applications

Ulrich Berger Orcid Logo

Logical Methods in Computer Science, Volume: 7, Issue: 1, Start page: 8

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

We give a coinductive characterization of the set of continuous functions defined on a compact real interval, and extract certified programs that construct and combine exact real number algorithms with respect to the binary signed digit representation of real numbers. The data type corresponding to...

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/cronfa7440
Tags: Add Tag
No Tags, Be the first to tag this record!
first_indexed 2013-07-23T11:58:20Z
last_indexed 2018-02-09T04:35:36Z
id cronfa7440
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2015-10-14T09:04:32.7485686</datestamp><bib-version>v2</bib-version><id>7440</id><entry>2012-02-23</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>2012-02-23</date><deptcode>SCS</deptcode><abstract>We give a coinductive characterization of the set of continuous functions defined on a compact real interval, and extract certified programs that 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. This is a pilot study in using proof-theoretic methods for certified algorithms in exact real arithmetic.</abstract><type>Journal Article</type><journal>Logical Methods in Computer Science</journal><volume>7</volume><journalNumber>1</journalNumber><paginationStart>8</paginationStart><publisher/><issnPrint>1860-5974</issnPrint><issnElectronic/><keywords>proof theory, program extraction, exact real number computation, coinduction</keywords><publishedDay>24</publishedDay><publishedMonth>3</publishedMonth><publishedYear>2011</publishedYear><publishedDate>2011-03-24</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>2015-10-14T09:04:32.7485686</lastEdited><Created>2012-02-23T17:01:55.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></authors><documents/><OutputDurs/></rfc1807>
spelling 2015-10-14T09:04:32.7485686 v2 7440 2012-02-23 From coinductive proofs to exact real arithmetic: theory and applications 61199ae25042a5e629c5398c4a40a4f5 0000-0002-7677-3582 Ulrich Berger Ulrich Berger true false 2012-02-23 SCS We give a coinductive characterization of the set of continuous functions defined on a compact real interval, and extract certified programs that 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. This is a pilot study in using proof-theoretic methods for certified algorithms in exact real arithmetic. Journal Article Logical Methods in Computer Science 7 1 8 1860-5974 proof theory, program extraction, exact real number computation, coinduction 24 3 2011 2011-03-24 10.2168/LMCS-7(1:8)2011 COLLEGE NANME Computer Science COLLEGE CODE SCS Swansea University 2015-10-14T09:04:32.7485686 2012-02-23T17:01:55.0000000 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Ulrich Berger 0000-0002-7677-3582 1
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
format Journal article
container_title Logical Methods in Computer Science
container_volume 7
container_issue 1
container_start_page 8
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 We give a coinductive characterization of the set of continuous functions defined on a compact real interval, and extract certified programs that 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. This is a pilot study in using proof-theoretic methods for certified algorithms in exact real arithmetic.
published_date 2011-03-24T03:09:14Z
_version_ 1763749873427939328
score 11.037603

Similar Items