JUCS - Journal of Universal Computer Science 16(18): 2535-2555, doi: 10.3217/jucs-016-18-2535
Realisability for Induction and Coinduction with Applications to Constructive Analysis
expand article infoUlrich Berger‡
‡ Swansea University, Swansea, United Kingdom

Corresponding author: Ulrich Berger ( u.berger@swansea.ac.uk )

© Ulrich Berger.
This article is freely available under the J.UCS Open Content License.
Citation: Berger U (2010) Realisability for Induction and Coinduction with Applications to Constructive Analysis. JUCS - Journal of Universal Computer Science 16(18): 2535-2555. https://doi.org/10.3217/jucs-016-18-2535
Open Access
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
realisability, program extraction, coinduction, constructive analysis