Efficient program synthesis from proofs

Monika Seisenberger

(Swansea University)

In this talk we aim to promote program synthesis from formal proofs as a powerful technique to obtain certified programs. We discuss and demonstrate the advantages of this method and show how it is supported by the interactive proof assistant Minlog.
Finally, we look at program extraction from coinductive proofs
and applications thereof where the efficiency of the method
also becomes visible in the effort needed for the formalisation.

Tuesday 6th October 2009, 14:00
Robert Recorde Room
Department of Computer Science