Sprungmarken

Servicenavigation

Hauptnavigation

Sie sind hier:

Hauptinhalt

Logische Methoden des Software Engineering

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

Aktuelles

Beschreibung

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:

  • Getypter Lambda Kalkül
  • Typinhabitation, Typinferenz, Typprüfung
  • Intuitionistische Logik
  • Klassische Logik
  • Logikmodelle
  • Curry-Howard-Isomorhismus (Korrespondenz zwischen Typen und logischen Formeln)
  • Kombinatorische Logik

Vorlesungsmaterial

Vorlesungsfolien werden semesterbegleitend berei und sind aus dem Campusnetz oder via VPN aufrufbar.

Folien

Übung

Bei Fragen zu den Übungen wenden Sie sich an Andrej Dudenhefner.

  • Die Übung dient der Verstetigung des Vorlesungsinhalts sowie der praktischen Anwendung der erlangten Kenntnisse.
  • Beweise werden zum Teil länger diskutiert und durch Aufgaben dargestellt.

Anmeldung

  • Bitte beachten Sie, dass Sie sich sowohl zu der Veranstaltung als auch zur Übung bei Andrej Dudenhefner anmelden müssen!

Übungsgruppen

Gruppe Zeit Ort Start Turnus
1 Donnerstag, 14-16 Uhr OH12, Raum 1.056 19.10.2017 wöchentlich

Übungszettel

Abgabe vor der Vorlesung im Vorlesungsraum beim Veranstalter

Studienleistung

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:

  • Aufgabenblätter sind den Blöcken 1 oder 2 zugeordnet
  • In jedem Block müssen mindestens 50% der erreichbaren Punkte erreicht werden
  • Blöcke 1 und 2 machen jeweils ungefähr die Hälfte aller Übungsblätter aus

Prüfungen



Nebeninhalt

Kontakt

Prof. Dr. Jakob Rehof
Lehrstuhlinhaber
Tel.: 0231 755-7951
M. Sc. Andrej Dudenhefner
Tel.: 0231 755-7738