Realisability and Adequacy for (Co)induction

Author Ulrich Berger



PDF
Thumbnail PDF

File

OASIcs.CCA.2009.2258.pdf
  • Filesize: 323 kB
  • 12 pages

Document Identifiers

Author Details

Ulrich Berger

Cite AsGet 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.
Keywords
  • Constructive Analysis
  • realisability
  • program extraction
  • semantics

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail