Proofs, Programs, Processes

Abstract. 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 w.r.t. to the binary signed digit representation.

• Type: Journal
• Year: 2010
• Where: CIE
• Authors: Ulrich Berger, Monika Seisenberger
• Keywords: Applied Computing, Binary Signed Digit, CIE 2010, Lazy Functional Programming, Processes Producing Infinite