No Cover Image

Book chapter 431 views

Proofs, Programs, Processes / Ulrich Berger; Monika Seisenberger

Programs, Proofs, Processes, Volume: 6158, Pages: 39 - 48

Swansea University Author: Ulrich, Berger

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

Abstract

<p>We study a realisability interpretation for inductive and coinductive definitions and discuss its application to program extraction from proofs. A speciality of this interpretation is that realisers are given by terms that correspond directly to programs in a lazy functional programming lan...

Full description

Published in: Programs, Proofs, Processes
ISSN: 0302-9743 1611-3349
Published: Berlin Springer 2010
Online Access: Check full text

URI: https://cronfa.swan.ac.uk/Record/cronfa5273
Tags: Add Tag
No Tags, Be the first to tag this record!
Abstract: <p>We study a realisability interpretation for inductive and coinductive definitions and discuss its application to program extraction from proofs. A speciality of this interpretation is that realisers are given by terms that correspond directly to programs in a lazy functional programming language such as Haskell. Programs extracted from proofs using coinduction can be understood as perpetual processes producing infinite streams of data. Typical applications of such processes are computations in exact real arithmetic. As an example we show how to extract a program computing the average of two real numbers with respect to the binary signed digit representation.</p>
Item Description: Lecture Notes in Computer Science Volume 6158
College: College of Science
Start Page: 39
End Page: 48