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: OH 12, Raum 1.056
Zeit: Mittwoch, 14-16 Uhr
Beginn: 26.10.2016
Anmeldung: Vorlesung und Übung: Boris Düdder

Aktuelles

  1. Die Übung am Donnerstag, 26.1.2017 entfällt.
  2. Termine für die mündliche Prüfung sind der 14.3. und 28.3.2017.

Beschreibung

Die Vorlesung wird die Themen Typentheorie und Typinferenz behandeln. Insbesondere Zusammenhänge zwischen Programmiersprachen und Subtypenrelationen werden näher besprochen werden, mit besonderer Berücksichtigung algorithmischer und komplexitätstheoretischer Aspekte.

Eine zentrale Fragestellung der Vorlesung wird die automatische Synthese von Programmen aus Komponentenbibliotheken mittels logischer Deduktion sein.

Die Vorlesung beginnt mit einer Einführung in den getypten Lambda Kalkül. Ausgehend von den vorgestellten einfachen Typen werden Typinferenz und verwandte Fragestellungen behandelt, insbesondere im Bereich der Subtypen. Es sollen in der Vorlesung und der Übung verschiedene wissenschaftliche Artikel zu den Vorlesungsthemen erarbeitet werden.

Vorlesungsfolien

Die Vorlesungsfolien sind aus dem Campusnetz oder über das VPN aufrufbar. Sie werden semesterbegleitend fortlaufend bereitgestellt, und zwar (planmäßig) spätestens um Mitternacht am Vorabend eines Vorlesungstages.

Im Anschluss daran kann es noch zu kleineren Änderungen kommen (z.B. das Hinzufügen der Antwort-Folien zu den während einer Vorlesung gestellten Diskussionfragen im Anschluss an eine Vorlesung).

Folien

  1. Einführung und Überblick
  2. Induktionsprinzipien, Newmans Lemma und Church-Rosser Satz
  3. Church Codierung und Berechnungsmächtigkeit
  4. Theorie des einfach getypten Lambdkalküls
  5. Church Style Typsystem und schwache Normalisierung
  6. Intuitionistische Logik und natürliche Deduktion
  7. Curry-Howard Isomorphismus
  8. Modelle der intuitionistischen Logik
  9. Starke Normalisierung
  10. Type Checking
  11. Kontrolloperatoren
  12. Lambda-Delta-Kalkül

Übung

Bei Fragen zu den Übungen und ihrer Durchführung kann sich an Boris Düdder gewandt werden.

  • Die Übung dient der Verstetigung des Vorlesungsinhalts sowie der praktischen Anwendung der erlangten Kenntnisse über die unterliegenden Grundlagen hinaus.
  • 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 Boris Düdder anmelden müssen!!!

Übungsgruppen

Gruppe Zeit Ort Start Turnus
1 Donnerstag, 10-12 Uhr OH14, Raum 104 3.11.2016 wöchentlich

Übungszettel

Abgabe bevor der Vorlesung im Vorlesungsraum OH12, Raum 1.056

Studienleistung

Das Erlangen der Studienleistung ist Voraussetzung für die Teilnahme an der abschließenden mündlichen Prüfung.
Die Kriterien sind wie folgt:

  • Erreichen von mind. 40% der Punkte aus den Hausübungen in der ersten Hälfte der Übungsblätter
  • Erreichen von mind. 40% der Punkte aus den Hausübungen in der zweiten Hälfte der Übungsblätter

Prüfungen

Die mündlichen Prüfungen finden am Dienstag,

  • 14.3.2017
  • 28.3.2017

statt. Die Anmeldung zu den Prüfungen erfolgen über das Sekretariat (Frau Joschko).

Leistungsnachweis

Studierende können einen Leistungsnachweis über diese Veranstaltung ablegen.
Dazu gelten folgende Kriterien:



Nebeninhalt

Kontakt

Prof. Dr. Jakob Rehof
Lehrstuhlinhaber
Tel.: 0231 755-7951
M. Sc. Jan Bessai
Tel.: 0231 755-7764
M. Sc. Andrej Dudenhefner
Tel.: 0231 755-7738
Dr. Boris Düdder