Estonian Winter Schools in Computer Science
Eesti arvutiteaduse talvekoolid
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.
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.
( http://uk.cambridge.org/computerscience/theoretical/catalogue/0521779111/ )
U. Berger, W. Buchholz, H. Schwichtenberg. Refined program extraction from classical proofs. *Preprint version* of the article in Ann. Pure Appl. Logic, v. 114, n. 1-3, pp. 3-25, 2002.
Slides from the lectures will be distributed after the school.
Modified Tuesday, Mar 06, 2018 at 16:54 EET+0200 by firstname.lastname@example.org