Journal article 1162 views
Realisability for Induction and Coinduction with Applications to Constructive Analysis
Journal of Universal Computer Science, Volume: 16, Issue: 18, Pages: 2535 - 2555
Swansea University Author:
Ulrich Berger
Full text not available from this repository: check for access using links below.
DOI (Published version): 10.3217/jucs-016-18-2535
Abstract
We prove the correctness of a formalised realisability interpretation of extensions of first-order theories by inductive and coinductive definitions in an untyped λ-calculus with fixed-points. We illustrate the use of this interpretation for program extraction by some simple examples in the area of...
| Published in: | Journal of Universal Computer Science |
|---|---|
| ISSN: | 0948-6968 |
| Published: |
2010
|
| Online Access: |
Check full text
|
| URI: | https://cronfa.swan.ac.uk/Record/cronfa7893 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Abstract: |
We prove the correctness of a formalised realisability interpretation of extensions of first-order theories by inductive and coinductive definitions in an untyped λ-calculus with fixed-points. We illustrate the use of this interpretation for program extraction by some simple examples in the area of exact real number computation and hint at further non-trivial applications in computable analysis. |
|---|---|
| Keywords: |
coinduction, constructive analysis, program extraction, realisability |
| College: |
Faculty of Science and Engineering |
| Issue: |
18 |
| Start Page: |
2535 |
| End Page: |
2555 |