Estonian Winter Schools in Computer Science    
Eesti arvutiteaduse talvekoolid
EWSCS 2002
EATTK 2002

7th Estonian Winter School in Computer Science (EWSCS)
VII Eesti Arvutiteaduse Talvekool (EATTK)

Palmse, Estonia
March 3 - 8, 2002

Prof. Helmut Schwichtenberg

Mathematisches Institut,
Ludwig-Maximilians-Universität München

Extracting Programs From Proofs


It is well known that it is undecidable in general whether a given program meets its specification. In contrast, it can be checked easily by a machine whether a formal proof is correct, and from a constructive proof one can automatically extract a corresponding program, which by its very construction is correct as well. This -- at least in principle -- opens a way to produce correct software, e.g. for safety-critical applications. Moreover, programs obtained from proofs are 'commented' in a rather extreme sense. Therefore it is easy to maintain them, and also to adapt them to particular situations. Dana Scott proposed the name 'proof mining' for such activities.

We will concentrate on the question to what extent classical proofs can be used, and how proofs systems should be designed to ensure feasibility of the extracted programs.

Course materials

For students unfamiliar with the basics of the subject it is strongly recommended that they read Chapters 1, 2 and 6 of A.S. Troelstra and H. Schwichtenberg: Basic Proof Theory, Cambridge University Press, 2nd edition 2000.
( )

About the Speaker


Modified Wednesday, Jun 27, 2018 at 10:24 EEST+0300 by