Theorie und Praxis der Extraktion von Programmen aus formalen Beweisen

• Applicant: Professor Dr. Helmut Schwichtenberg
• Subject Area: Theoretical Computer Science
• Term: from 2005 to 2007
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 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 Programme: Research Grants