Extraktion effizienter Programme aus formalen Beweisen

• Antragsteller: Professor Dr. Helmut Schwichtenberg
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2000 bis 2001
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 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-Verfahren: Sachbeihilfen