Theorie und Praxis der Extraktion von Programmen aus formalen Beweisen

• Antragsteller: Professor Dr. Helmut Schwichtenberg
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2005 bis 2007
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 19227859

Es ist bekannt, dass sich Programme aus formalen Beweisen extrahieren lassen. Die theoretischen Grundlagen hierzu und die in Anwendungen auftretenden Probleme sollen unter folgenden Aspekten und in den folgenden Bereichen untersucht werden: (1) Approximierbare Funktionale in der Typentheorie, (2) Effizienz der extrahierten Programme, (3) Programmextraktion aus klassischen Beweisen, mit besonderer Berücksichtigung der Rolle von Fixpunkt- und Kontrolloperatoren, und (4) Konstruktive Analysis. Parallel dazu soll die prototypische Implementierung MINLOG weiterentwickelt und damit Fallstudien durchgeführt werden.

• DFG-Verfahren: Sachbeihilfen