Extraktion effizienter Programme aus formalen Beweisen

• Applicant: Professor Dr. Helmut Schwichtenberg
• Subject Area: Theoretical Computer Science
• Term: from 2000 to 2001
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 5274986

Es ist bekannt, daß sich Programme aus formalen Beweisen extrahieren lassen. Die theoretischen Grundlagen hierzu sollen unter folgenden Aspekten untersucht werden. 1. Effizienz der extrahierten Programme; 2. Programmextraktion aus klassischen Beweisen, mit besonderer Berücksichtigung der rolle von Fixpunkt- und Kontrolloperatoren, und 3. Einbeziehung der Beweistheorie undendlicher Herleitungen Parallel dazu soll die prototypische Implementierung MINLOG weiterentwickelt und damit Fallstudien durchgeführt werden.

• DFG Programme: Research Grants