Go home now Header Background Image
Submission Procedure
share: |
Follow us
Volume 16 / Issue 18

available in:   PDF (204 kB) PS (314 kB)
Similar Docs BibTeX   Write a comment
Links into Future
DOI:   10.3217/jucs-016-18-2535


Realisability for Induction and Coinduction with Applications to Constructive Analysis

Ulrich Berger (Swansea University, United Kingdom)

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

Categories: F.3, F.3.1, F.3.2