Extraktion effizienter Programme aus formalen Beweisen

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