Chiarabini, Luca (2009): Program Development by Proof Transformation. Dissertation, LMU München: Faculty of Mathematics, Computer Science and Statistics 

PDF
Chiarabini_Luca.pdf 1MB 
Abstract
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 semiautomatic 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 socalled "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 adhoc 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 semiautomatic 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.
Item Type:  Thesis (Dissertation, LMU Munich) 

Subjects:  500 Natural sciences and mathematics > 510 Mathematics 500 Natural sciences and mathematics 
Faculties:  Faculty of Mathematics, Computer Science and Statistics 
Language:  English 
Date of oral examination:  18. December 2009 
1. Referee:  Heun, Volker 
MD5 Checksum of the PDFfile:  46f4096bd1f56b640ce2782dd5797b14 
Signature of the printed copy:  0001/UMC 18318 
ID Code:  11064 
Deposited On:  03. Feb 2010 13:25 
Last Modified:  19. Jul 2016 16:28 