Program Extraction From Proofs: Induction and Coinduction

Ulrich Berger

(Swansea University)

In this talk I give two examples of program extraction from proofs in a constructive theory of inductive and coinductive definitions. The first belongs to the realm of computable analysis. A coinductive predicate C0 is defined characterising those real numbers that are constructively "approximable". From proofs of closure properties of C0 one extract implementations of arithmetic operations with respect to the signed digit representation of real numbers. In the second example I show how to extract monadic parser combinators (Hutton and Meijer) from proofs that certain labelled transition systems are finitely branching. While in the first example coinduction is central, here induction features prominently because finiteness is an inductive concept. Both examples have in common that the data types the extracted programs operate on (infinite digit streams, higher-order functions) are not present in the (source) proofs which reside in simple extensions of first-order logic. This indicates that the perspective of replacing programming by the activity of proving is not as daunting as it seems, and that therefore program extraction might become an attractive method for producing formally certified programs in the future.
Thursday 4th March 2010, 14:00
Video conferencing room - Far 134
Department of Computer Science