Program extraction from coinductive proofs and its application to exact real arithmetic
Miyamoto, Kenji · Elektronische Hochschulschriften der LMU München (Ludwig-Maximilians-Universität München) · 2013
Program extraction has been initiated in the field of constructive mathematics, and it attracts interest not only from mathematicians but also from computer scientists nowadays. From a mathematical viewpoint its aim is to figure out computational meaning of proofs, while from a computer-scientific viewpoint its aim is the study of a method to obtain correct programs. Therefore, it is natural to have both theoretical results and a practical computer system to develop executable programs via program extraction. In this Thesis we study the computational interpretation of constructive proofs involving inductive and coinductive reasoning. We interpret proofs by translating the computational content of proofs into executable program code. This translation is the procedure we call program extraction and it is given through Kreisel's modified realizability. Here we study a proof-theoretic foundation for program extraction, enriching the proof assistant system Minlog based on this theoretical improvement. Once a proof of a formula is written in Minlog, a program can be extracted from the proof by the system itself, and the extracted program can be executed in Minlog. Moreover, extracted programs are provably correct with respect to the proven formula due to a soundness theorem which we prove. We practice program extraction by elaborating some case studies from exact real arithmetic within our formal theory. Although these case studies have been studied elsewhere, here we offer a formalization of them in Minlog, and also machine-extraction of the corresponding programs.