JAIST Logic@JAIST

Extracting programs from proofs

  • Prof. Dr. Helmut Schwichtenberg

  • Ludwig-Maximilians-Universitaet Muenchen, Germany

  • Homepage
Date: 2014/03/07 (Fri) 15:10 to 16:40
Place: JAIST, Lecture room I1
Group: Logic Unit
Every constructive proof of an existential theorem (or problem; Kolmogorov 1932) contains a construction of a solution. To get hold of such a solution we have two methods. (a) Write-and-verify. Guided by the constructive proof directly write a program to compute the solution, and then prove (verify) that this is the case. (b) Prove-and-extract. Formalize the proof and extract its computational content in the form of a realizing term t. Since the latter approach requires formalization of the proof it is less popular. But it has advantages. (i) Dealing with a problem on the proof level allows abstract mathematical tools and a good organization of the material. Both help to adapt the proof to changed specifications. (ii) The extracted term can be automatically verified, by means of a formalization of the soundness theorem. As an example of the prove-and-extract method we build a parser for the Dyck language of balanced parentheses.
Contact Hajime Ishihara