| Veranstalter: |
Dr. Lukasz Czajka |
Kontaktperson für
organisatorische Fragen: |
Christoph Stahl |
| Veranstaltungsnummer: |
042357 (Vorlesung)
042358 (Übung) |
| Typ: |
Vertiefungsmodul |
| Modulnummer: |
INF-MSc-326 |
| SWS: |
2 SWS Vorlesung
1 SWS Übung
1 SWS Praktikum |
| Ort: |
Online |
| Zeit: |
Montags: 10-12
Mittwochs: 14-16 |
| Beginn: |
04.01.2021 |
| Ende: |
10.02.2021 |
Aktuelles
- Schreibt Euch in den Moodlekurs ein.
- Weitere Informationen folgen im Verlauf des Semesters.
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)
Bemerkungen
- Ehemals als "Komponenten- und Service-Orientierte Softwarekonstruktion" angeboten
- LMSE 2 findet in der zweiten Hälfte der Vorlesungszeit statt
- LMSE 2 kann in vorheriger Kombination mit LMSE 1 innerhalb eines Semesters belegt und geprüft werden
Vorlesungsmaterial
Vorlesungsfolien werden semesterbegleitend berei und sind aus dem Campusnetz oder via VPN aufrufbar.
Ü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
- Die Übungen können ohne Anmeldung besucht werden.
- Die Startdaten sind noch vorläufig.
Übungsgruppen
| Gruppe |
Zeit |
Ort |
Start |
Turnus |
| 1 |
Montag, 12-14 Uhr |
Online |
11.01.2020 |
wöchentlich |
| 2 |
Mittwoch, 12-14 Uhr |
Online |
13.01.2020 |
wöchentlich |
Praktikum
Das Praktikum dient der praktischen Umsetzung der in der Vorlesung erlangten Kenntnisse. Dabei soll in Gruppen jeweils eine Beweisaufgabe gelöst werden, die im direkten Zusammenhang zum Vorlesungsinhalt (insb. Lambda-Kalkül) steht.
- Die verwendete Programmiersprache ist Coq
- Die gemeinsamen Ergebnisse des Praktikums werden im folgenden git Repository verwaltet.
- Die Zuordnung der Aufgaben inkl. Rechtevergabe am Repository findet in der zweiten Vorlesungswoche statt
- Zum erfolgreichen bestehen des Praktikums gehören:
- Formales Beweisen der unter der jeweiligen Aufgaben angegebenen Aussagen
- Wiki-Eintrag mit Beschreibung der bewiesenen Aussage inkl. einer informellen Beweisskizze
- Kurze Vorstellung der Lösung bei der Abschlusspräsentation der Praktikumsprojekte durch ein Mitglied der jeweiligen Gruppe (10 Minuten, keine Folien)
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
- Wird noch bekannt gegeben. Findet in der Vorlesungsfreien Zeit zusammen mit LMSE1 statt.
