Sprungmarken

Servicenavigation

Hauptnavigation

Sie sind hier:

Hauptinhalt

Logische Methoden des Software Engineering 2

Veranstalter: Prof. Dr. Jakob Rehof
Kontaktperson für
organisatorische Fragen:
Andrej Dudenhefner
Veranstaltungsnummer: 042357 (Vorlesung)
042358 (Übung)
Typ: Vertiefungsmodul
Modulnummer: INF-MSc-312
SWS: 2 SWS Vorlesung
1 SWS Übung
1 SWS Praktikum
Ort: OH12, E.003
Zeit: Montag 10-12 Uhr
Mittwoch 14-16 Uhr
Beginn: 26.11.2018
Ende: 30.01.2019

Aktuelles

  • LMSE 2 kann mit vorheriger Kombination mit LMSE 1 innerhalb eines Semesters belegt und geprüft werden

Beschreibung

Die Vorlesung LMSE 2 behandelt das Thema Typentheorie und deren Verbindung zur mathematischen Logik. Das zentrale Resultat der Typentheorie ("Curry-Howard-Isomporphismus") zeigt die Korrespondenz zwischen Typen und logischen Formeln, sowie zwischen Programmen und logischen Beweisen.

Es werden über den LMSE 1 Inhalt hinaus weitere Typsysteme (Intersektionstypsystem, System F, Dependent Types, Pure Type Systems) und damit verbundene logische Ausdrucksmächtigkeit betrachtet. Dabei muss der Lambda-Kalkül erweitert werden, um Berechnungen sowohl auf Termebene, als auch auf Typebene zu ermöglichen.

Diese Erweiterung erlaubt in der Praxis mechanisch verifizierbare Beweise über funktionale Programme mittels Typtheorie zu führen.

Die Vorlesung LMSE 2 umfasst folgende Themen:

  • Lambda Kalkül mit Intersektionstypen und starke Normalisierung
  • System F und intuitionistische Logik zweiter Stufe
  • Dependent Types und Programmkorrektheisbeweise
  • Mechanisierung mathematischer Beweise 🤖
  • Curry-Howard-Isomorhismus (Korrespondenz zwischen Typen und logischen Formeln)

Vorlesungsmaterial

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

Folien

Übung

  • Die Übung zu LMSE 2 ist eine Präsenzübung (keine Anwesenheits- oder Abgabepflicht).
  • Die Übung dient der Verstetigung des Vorlesungsinhalts sowie der praktischen Anwendung der erlangten Kenntnisse.
  • Beweise werden zum Teil länger diskutiert und anhand von Beispielen untersucht.

Anmeldung

  • wird in der ersten Vorlesungswoche bekanntgegeben

Übungsgruppen

Gruppe Zeit Ort Start Turnus
1 Dienstag, 10-12 Uhr OH12, Raum 2.063 27.11.2018 wöchentlich
2 Donnerstag, 12-14 Uhr OH12, Raum 2.063 29.11.2018 wöchentlich

Übungszettel

Praktikum

Das Praktikum dient der praktischen Umsetzung der in der Vorlesung erlangten Kenntnisse. Dabei soll in Gruppen jeweils eine formale Beweisaufgabe in der Beweissprache Coq gelöst werden, die im direkten Zusammenhang zum Vorlesungsinhalt (insb. Lambda-Kalkül) steht.

Studienleistung

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

  • erfolgreich abgeschlossenes Praktikumsprojekt

Klausuren



Nebeninhalt

Kontakt

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