Ulrich Berger (Swansea, UK), Extracting concrete programs from abstract mathematics
Schedule
- Feb. 13, 2012, 15:00 - 16:00
Abstract
In this talk I will argue that in order to extract correct and useful
programs from mathematical proofs it is often not necessary to
completely formalize the objects considered, but only certain
carefully chosen aspects of them. This makes the formalization of
mathematical objects and proofs for the purpose of program extraction
a much less daunting enterprise than one might expect, and brings this
method of certified program development closer to practical
applications. I will illustrate this by means of examples in
constructive analysis.
Attachments
In this talk I will argue that in order to extract correct and useful programs from mathematical proofs it is often not necessary to completely formalize the objects considered, but only certain carefully chosen aspects of them. This makes the formalization of mathematical objects and proofs for the purpose of program extraction a much less daunting enterprise than one might expect, and brings this method of certified program development closer to practical applications. I will illustrate this by means of examples in constructive analysis.