Program Extraction for Exact Real Arithmetic

Kenji Miyamoto

(LMU Munich)

In this talk, I show a case study of program extraction on exact real arithmetic. We constructively prove a proposition on two real numbers and from the proof we obtain an average function by our program extraction mechanism. The representation of real numbers in the program is the signed digit stream which also comes from the extraction mechanism. We have a formalized proof of this case study on the proof system Minlog. The extracted program is available on Minlog to execute. This work is a joint work with Prof. Helmut Schwichtenberg in Munich.

Keywords: Coinduction, Corecursion, Program Extraction, Exact Real Arithmetic.
Thursday 29th March 2012, 14:00
Robert Recorde Room
Department of Computer Science