No Cover Image

Journal article 385 views

Realisability for Induction and Coinduction with Applications to Constructive Analysis / Ulrich, Berger

Journal of Universal Computer Science, Volume: 16, Issue: 18, Pages: 2535 - 2555

Swansea University Author: Ulrich, Berger

Full text not available from this repository: check for access using links below.

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...

Full description

Published in: Journal of Universal Computer Science
ISSN: 0948-6968
Published: 2010
Online Access: Check full text

URI: https://cronfa.swan.ac.uk/Record/cronfa7893
Tags: Add Tag
No Tags, Be the first to tag this record!
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
College: College of Science
Issue: 18
Start Page: 2535
End Page: 2555