Veranstalter: | Prof. Dr. Jakob Rehof |
---|---|
Veranstaltungsnummer: | 042343 (Vorlesung) 042344 (Übung) |
Typ: | Vertiefungsmodul |
Modulnummer: | INF-MSc-319 |
SWS: | 2 SWS Vorlesung 2 SWS Übung |
Ort: | OH12, Raum 1.056 |
Zeit: | Mittwoch, 14-16 Uhr |
Beginn: | 11.10.2017 |
Anmeldung: | Vorlesung und Übung: Andrej Dudenhefner |
Die Vorlesung wird das Thema Typentheorie und deren Verbindung zur mathematischen Logik behandeln. Durch klassische Resultate der Typtheorie ("Curry-Howard-Isomporphismus") lassen sich Typen als logische Formel betrachten und Programme als Beweisstrukturen in der typtheoretischen Logik.
Typen können dem zufolge als logische Spezifikationen verstanden werden, wobei z.B. logische Verfahren benutzt werden können, um Programme zu generieren, die solche Spezifikationen erfüllen ("Programmextraktion"). Die Vorlesung wird folgende Themen näher behandeln:
Vorlesungsfolien werden semesterbegleitend berei und sind aus dem Campusnetz oder via VPN aufrufbar.
Bei Fragen zu den Übungen wenden Sie sich an Andrej Dudenhefner.
Gruppe | Zeit | Ort | Start | Turnus |
---|---|---|---|---|
1 | Donnerstag, 14-16 Uhr | OH12, Raum 1.056 | 19.10.2017 | wöchentlich |
Abgabe vor der Vorlesung im Vorlesungsraum beim Veranstalter
Das Erlangen der Studienleistung ist Voraussetzung für die Teilnahme an der abschließenden mündlichen Prüfung.
Die Kriterien der Studienleistung sind wie folgt: