OASIcs.CCA.2009.2258.pdf
- Filesize: 323 kB
- 12 pages
Document
Realisability and Adequacy for (Co)induction
Author
-
Part of:
Volume:
6th International Conference on Computability and Complexity in Analysis (CCA'09) (CCA 2009)
Series: Open Access Series in Informatics (OASIcs) - License:
Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
- Publication Date: 2009-11-25
Cite As Get BibTex
Ulrich Berger. Realisability and Adequacy for (Co)induction. In 6th International Conference on Computability and Complexity in Analysis (CCA'09). Open Access Series in Informatics (OASIcs), Volume 11, pp. 49-60, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)
https://doi.org/10.4230/OASIcs.CCA.2009.2258
Abstract
We prove the correctness of a formalised realisability interpretation of extensions of first-order theories by inductive and coinductive definitions in an untyped $\lambda$-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.
Subject Classification
Keywords
- Constructive Analysis
- realisability
- program extraction
- semantics
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads