Sciweavers

Share
JUCS
2010

Realisability for Induction and Coinduction with Applications to Constructive Analysis

8 years 8 months ago
Realisability for Induction and Coinduction with Applications to Constructive Analysis
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. Key Words: realisability, program extraction, coinduction, constructive analysis Category: F.3, F.3.1, F.3.2
Ulrich Berger
Added 20 May 2011
Updated 20 May 2011
Type Journal
Year 2010
Where JUCS
Authors Ulrich Berger
Comments (0)
books