|
||||
|
||||
Übersicht |
||||
Die Vorlesung Automatisierte Logik und Programmierung richtet
sich an Studenten des Hauptstudiums Informatik mit einem Interesse
für den Einsatz formal-logischer Methoden in der Programmierung.
Aufgrund der Vielzahl aufeinander aufbauender Themen erstreckt sich die
Veranstaltung über zwei Semester.
Der erste Teil befasst sich mit der Formalisierung von Logik, Berechenbarkeit und Datentypen sowie den zugehörigen Kalkülen, während im zweiten Teil die Implementierung von Beweissystemen, die Automatisierung logischer Schlüsse und die Synthese von Algorithmen aus formalen Spezifikationen im Vordergrund steht. Dabei wird ein besonderer Schwerpunkt auf die intutionistische Typentheorie und das interaktive Beweissystem NuPRL gelegt. Thematisch ist die Veranstaltung sowohl in der Theoretischen als auch in der Angewandten Informatik angesiedelt, wobei der erste Teil die Theorie etwas stärker betont und der zweite Teil die Anwendung von Theorie bei der Entwicklung zuverlässiger Software. |
Vorlesungsfolien | |||||
Vollständiges Skriptum (350 Seiten) | |||||
Kapitel 1: Einführung
|
PS | PS (2:1) | |||
Kapitel 2: Formalisierung von Logik, Berechenbarkeit und Typdisziplin
|
PS | PS (2:1) | |||
Kapitel 3: Die Intuitionistische Typentheorie
|
PS | PS (2:1) | |||
Kapitel 4: Automatisierung des formalen Schliessens
|
PS | PS (2:1) | |||
Kapitel 5: Automatisierte Softwareentwicklung
|
PS | PS (2:1) | |||
Anhang A: Typentheorie: Syntax, Semantik, Inferenzregeln
|
PS | PS (2:1) | |||
Anhang B: Konservative Erweiterungen der Typentheorie und ihre Gesetze
|
PS | PS (2:1) | |||
Literaturverzeichnis
|
PS | PS (2:1) | |||
Back to overview of courses |