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
 

Projektbeschreibung

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