Theorie und Praxis der Extraktion von Programmen aus formalen Beweisen
Zusammenfassung der Projektergebnisse
Es ist bekannt, daß sich Programme aus formalen Beweisen extrahieren lassen. Die theoretischen Grundlagen hierzu und die in Anwendungen auftretenden Problerne wurden unter folgenden Aspekten und in den folgenden Bereichen untersucht: (1) Approximierbare Funktionale in der Typentheorie, (2) Effizienz der extrahierten Programme, und (3) Konstruktive Analysis. Parallel dazu wurde die prototypische Implementierung MiNLOG eines interaktiven und für die Programmextraktion besonders geeigneten Bewiesassistenten weit er entwickelt und damit Fallstudien durchgeführt. Zu der erfolgreichen Arbeit an der Universität Uppsala in Schweden hat neben der Gastfreundschaft, des dortigen mathematischen Instituts auch die im Vergleich mit Deutschland wesentlich bessere finanzielle Ausstattung der Universität beigetragen; dies war etwa in dem Bestand der Bibliothek deutlich festzustellen. Für die Unterstützung durch DFG, die diesen Fortschungsaufenthalt ermöglicht hat, möchte ich mich auch an dieser Stelle herzlich bedanken.
Projektbezogene Publikationen (Auswahl)
- An arithmetic for polynomial-time computation, Theoretical Computer Science 357 (2006), 202-214.
- Inverting monotone continuous functions in constructive analysis, Logical Approaches to Computational Barriers. (Proc. CiE 2006, Swansea) (B Loewe A Beckmann, U Berger and J V Tucker, eds.), LNCS, vol. 3988, Springer Verlag. Berlin, Heidelberg, New York, 2006, pp. 490- 504.
- Minlog, The Seventeen Provers of the World (F. Wiedijk, ed.), LNAI, vol. 3600, Springer Verlag, 2006, pp. 151-157.
- Recursion on the partial continuous functionals, Logic Colloquium '05 (C. Dimitracopoulos, L. Newelski, D. Normann, and J. Steel, eds.), Lecture Notes in Logic, vol. 28, Association for Symbolic Logic, 2006, pp. 173-201
- Ulrich Berger, Stefan Berghofer, Pierre Letouzey. and Helmut Schwichtenberg, Program extraction from normalization proofs, Studia Logica 82 (2006), 27-51.
