No Cover Image

Journal article 388 views

Proofs, Programs, Processes / Ulrich, Berger; Monika, Seisenberger

Theory of Computing Systems, Volume: 51, Issue: 3, Pages: 313 - 329

Swansesa University Authors: Ulrich, Berger, Monika, Seisenberger

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

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

Full description

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: College of Science
Issue: 3
Start Page: 313
End Page: 329