Theorie und Praxis der Extraktion von Programmen aus formalen Beweisen

点击翻译按钮获取中文摘要

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.