Journal article 1181 views
From coinductive proofs to exact real arithmetic: theory and applications
Logical Methods in Computer Science, Volume: 7, Issue: 1, Start page: 8
Swansea University Author:
Ulrich Berger
Full text not available from this repository: check for access using links below.
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...
| 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!
|
| 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. |
|---|---|
| Keywords: |
proof theory, program extraction, exact real number computation, coinduction |
| College: |
Faculty of Science and Engineering |
| Issue: |
1 |
| Start Page: |
8 |