| Veranstalter: |
Dr. Lukasz Czajka |
Kontaktperson für
organisatorische Fragen: |
Christoph Stahl |
| Veranstaltungsnummer: |
042353 (Vorlesung)
042354 (Übung) |
| Typ: |
Vertiefungsmodul |
| Modulnummer: |
INF-MSc-325 |
| SWS: |
2 SWS Vorlesung
1 SWS Übung
1 SWS Praktikum |
| Ort: |
Online |
| Zeit: |
Montags: 10-12 Uhr
Mittwochs: 14-16 Uhr |
| Beginn: |
02.11.2020 |
| Ende: |
16.12.2020 (vorläufig) |
Aktuelles.
- Der Start der Vorlesung wurde um eine Woche nach hinten verschoben. Das alte Datum war: 26.10.2020. Das neue Datum ist: 02.11.2020. Auch die Übungen beginnen eine Woche später am 09.11.2020.
- Schreibt Euch in den Moodlekurs ein.
- Die Übungsanmeldung wird innerhalb der ersten Vorlesungswoche im AsSESS freigeschaltet.
Beschreibung
Die Vorlesung LMSE 1 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 zentrale Fragestellungen (Typinhabitation, Typprüfung) von Programmiersprachen in Zusammenhang mit zentralen Fragestellungen (Beweisbarkeit, Beweisprüfung) der formalen Logik gebracht. Dabei spielt der Lambda-Kalkül sowohl die Rolle einer Turing-vollständigen funktionalen Programmiersprache als auch einer logischen Beweissprache.
Die Vorlesung LMSE 1 umfasst folgende Themen:
- Ungetypter Lambda-Kalkül als Turing-vollständiges Berechnungsmodell
- Intuitionistische Logik
- Einfach getypter Lambda Kalkül
- Typinhabitation, Typinferenz, Typprüfung
- Curry-Howard-Isomorhismus (Korrespondenz zwischen Typen und logischen Formeln)
- Kombinatorische Logik
Bemerkungen
- Ehemals als "Logische Methoden des Software Engineering" angeboten
- LMSE 1 findet in der ersten Hälfte der Vorlesungszeit statt
- LMSE 1 kann in anschließender Kombination mit LMSE 2 innerhalb eines Semesters belegt und geprüft werden
Vorlesungsmaterial
Vorlesungsfolien werden semesterbegleitend bereitgestellt und sind aus dem Campusnetz oder via VPN aufrufbar.
Übung
- Die Übung zu LMSE 1 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 Übungsanmeldung wird innerhalb der ersten Vorlesungswoche im AsSESS freigeschaltet.
Übungsgruppen
| Gruppe |
Zeit |
Ort |
Start |
Turnus |
| 1 |
Montag, 12-14 Uhr |
Online |
09.11.2020 |
wöchentlich |
| 2 |
Mittwoch, 12-14 Uhr |
Online |
11.11.2020 |
wöchentlich |
Praktikum
Das Praktikum dient der praktischen Umsetzung der in der Vorlesung erlangten Kenntnisse. Dabei soll in Gruppen jeweils eine Programmieraufgabe 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:
- Implementierung der unter der jeweiligen Aufgaben angegebenen Funktion(en)
- Wiki-Eintrag mit Beschreibung der implementierten Funktion(en) inkl. Ein- und Ausgabeverhalten und ggf. wichtiger Eigenschaften
- Verargumentierung der Korrektheit der Implementierung (es sind keine Beweise verlangt) z.B. durch Ein-/Ausgabetests in einer separaten Datei (z.B. Aufgabe1Test.v)
- 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 LMSE2 statt.
