Zwischen bestimmten Programmiersprachen und Logiken besteht ein sehr enger Zusammenhang. Dort entsprechen Aussagen in der Logik den Typen in der Programmiersprache und Programme sind nichts anderes als Beweise. Die Ausführung eines Programms entspricht der Vereinfachung eines Beweises.

Die Konsequenzen sind beachtlich. Aus Sicht der Informatik können wir versuchen, die Anforderungen in Form von Typen zu schreiben. Ein Programm, welches mit diesen Typen arbeitet, ist dann automatisch der formale Beweis, dass wir die Anforderungen korrekt umgesetzt haben (aus diesem Zusammenhang ergibt sich auch der Titel der Vorlesung). Die ist aus Sicht der Qualitätssicherung optimal. Eine Programmverifikation über Tests mit einer naturgemäß beschränkten Aussagekraft ist dann überflüssig. Diese kann auch ein interessanter Ansatz für den Einsatz einer generativen AI sein. Wenn die AI ein Programm findet, welches mit den vorgegebenen Typen arbeitet, dann ist es automatisch korrekt.

In der Vorlesung werden wir betrachten, warum der als "Proposition as Types" bezeichnete Zusammenhang zwischen funktionalen Programmiersprachen und Logiken gilt. Wir werden dann logische Verknüpfungen auf Typen abbilden und Beweise programmieren. Dabei nutzen wir einen konstruktiven Ansatz und können dabei unsere gewohnte Arbeitsweise aus der Informatik anwenden. Auf der Basis geeigneter Typen (dependent types) werden wir dann die formale Korrektheit von Programmen beweisen.

Beweisunterstützungssysteme und "Proposition as Types" sind ein aktuelles Thema in der Programmiersprachenforschung. Ideen aus diesem Bereich werden in fünf bis zehn Jahren ihren Weg in gängige Programmiersprachen finden. Der wesentliche Aspekt ist aber, dass wir im Rahmen dieser Vorlesung ganz neue Einsichten in die Prorgammierung im Allgemeinen erlangen.

Themen

1	Einführung in die funktionale Programmierung (Haskell)
2	Lambda-Kalkül und Typisierung
3	Natürliches Schließen
4	Proposition as Types
5	Agda
6	Dependent Types
7	Korrektheit von Programmen