Journal article 1087 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 |