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.