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. © 2010 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Berger, U., & Seisenberger, M. (2010). Proofs, programs, processes. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6158 LNCS, pp. 39–48). https://doi.org/10.1007/978-3-642-13962-8_5
Mendeley helps you to discover research relevant for your work.