Extraction and verification of programs by analysis of formal proofs

AbstractMathematical proofs often implicity contain constructions of objects with certain properties. Our new program synthesis algorithm starts with a formal proof of size n, and in time O(n3) explicitly gives those constructions as a computer program. Termination and correctness are proved metamathematically (“program verification”). Furthermore, the region of algorithmically relevant formulae of a proof is characterized. Proofs outside this region may be inconstructive. A mathematical tool for the proof of termination and correctness is the proof-theoretical strong normalization. Graphs of symbols belonging together are constructed. From these the elementary program statements are read off