Program Development by Proof Transformation

In the last 20 years the formal approach to the development of software turned out to be a crucial technique for the generation of correct programs. This idea has its theoretical base into the several semi-automatic methods to transform a formal specification that describe the behavior of a program into an effective executable piece of code. One of this is the so-called "program extraction from proof". The idea is that from an constructive proof of a formula "for each x there exists y such that P(x,y)" we can automatically extract a program "t" such that the property P(x,t(x)) hold. In our days such proofs are normally written by ad-hoc tools (some of them are: COQ, ISABLLE, MINLOG, PX, AGDA, etc...) called "proof assistants". Even if today this technique is pretty well established, the "manipulation" of proofs in order to develop performing programs did not received big attention. In this thesis we will develop several automatic and semi-automatic methods in order to extract efficient code from constructive proofs. Our field of application will be computational biology, a research field in which the development of efficient programs is crucial. So our main goal will be to show how the manipulation of formal proofs, essentially studied by proof theorist, has a big effect also in practical program generation