Journal article 1327 views
Proofs, Programs, Processes
,
Monika Seisenberger
Theory of Computing Systems, Volume: 51, Issue: 3, Pages: 313 - 329
Swansea University Authors:
Ulrich Berger , Monika Seisenberger
Full text not available from this repository: check for access using links below.
DOI (Published version): 10.1007/s00224-011-9325-8
Abstract
The objective of this paper is to provide a theoretical foundation for program extraction from proofs. We give a realizability interpretation for first-order proofs involving inductive and coinductive definitions and discuss its application to the synthesis of provably correct programs. We show that...
| Published in: | Theory of Computing Systems |
|---|---|
| ISSN: | 1432-4350 1433-0490 |
| Published: |
2012
|
| Online Access: |
Check full text
|
| URI: | https://cronfa.swan.ac.uk/Record/cronfa7438 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Abstract: |
The objective of this paper is to provide a theoretical foundation for program extraction from proofs. We give a realizability interpretation for first-order proofs involving inductive and coinductive definitions and discuss its application to the synthesis of provably correct programs. We show that realizers, although per-se untyped, can be assigned polymorphic recursive types and hence represent valid 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 w.r.t.\ to the binary signed digit representation. |
|---|---|
| Keywords: |
program extraction, realizability, coinduction, verified programs, exact real number computation |
| College: |
Faculty of Science and Engineering |
| Issue: |
3 |
| Start Page: |
313 |
| End Page: |
329 |