Book chapter 1557 views
Proofs, Programs, Processes
Ulrich Berger 
,
Monika Seisenberger
,
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.
DOI (Published version): 10.1007/978-3-642-13962-8_5
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...
| 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 |
| 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: |
Faculty of Science and Engineering |
| Start Page: |
39 |
| End Page: |
48 |