Realisability and Adequacy for (Co)induction

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.

• Type: Conference
• Year: 2009
• Where: CCA
• Authors: Ulrich Berger
• Keywords: CCA 2009, Coinductive Definitions, Exact Real Number, Realisability Interpretation, Theoretical Computer Science