Ulrich Berger (Swansea, UK), Extracting concrete programs from abstract mathematics


  • Feb. 13, 2012, 15:00 - 16:00


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.