Aktuelles

• Die Klausureinsicht für die Zweitklausur findet am Montag, den 25.03.2019 von 10:00 bis 11:00 Uhr in OH12/R2.013 statt.
• Die vorläufige Notenübersicht der Zweitklausur befindet sich hier.
• Am Mittwoch, den 07.11.2018 fällt die Vorlesung aufgrund der Fachschaftsvollversammlung aus.
• Am Donnerstag, den 01.11.2018 fällt die Übung aufgrund des Feiertags aus. Selbsverständlich kann stattdessen die Dienstagsübung besucht werden.
• Die Abschlusspräsentation der Praktikumsprojekte findet am Mittwoch, dem 21.11.2018 an Stelle der Vorlesung statt. Mindestens ein Mitglied jeder Gruppe muss für die Vorstellung seiner Arbeit anwesend sein.
• Die Aufgabenverteilung des Praktikums befindet sich im Wiki
• Bitte jeweils Nutzername/Email des Accounts bei https://ls14-scm.cs.tu-dortmund.de bis Freitag, den 19.10.2018 um 12:00 Uhr an Andrej Dudenhefner schicken, um einem Praktikumsprojekt zugeordnet zu werden.
• Die Übungsanmeldung ist in AsSESS freigeschaltet. Die Anmeldefrist ist Freitag, der 12.10.2018 um 12:00 Uhr.
• Am Mittwoch, den 24.10.2018 findet die Vorlesung in SRG1/1.001 statt.

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 berei und sind aus dem Campusnetz oder via VPN aufrufbar.

• Lectures on the Curry-Howard Isomorphism by Morten Heine B. Sorensen and Pawel Urzyczyn
• Lambda Calculi with Types by Henk Barendregt
• Strong Normalization and Typability with Intersection Types by Silvia Ghilezan
• Towards Combinatory Logic Synthesis by Jakob Rehof
• Combinatory Logic and Program Synthesis by Jakob Rehof

Folien

• Einführung und Überblick
• Induktionsprinzipien, Newmans Lemma und Church-Rosser Satz
• Church Codierung und Berechnungsmächtigkeit
• Theorie des einfach getypten Lambdkalküls
• Church Style Typsystem und schwache Normalisierung
• Intuitionistische Logik und natürliche Deduktion
• Curry-Howard Isomorphismus
• Modelle der intuitionistischen Logik
• Starke Normalisierung
• Unifikation und Type Checking
• Beweisbarkeit und Inhabitation
• Kombinatorische Logik

Ü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 ist in AsSESS freigeschaltet. Die Anmeldefrist ist Freitag, der 12.10.2018 um 12:00 Uhr.

Übungsgruppen

Übungsblätter

• Übungsblatt 01
• Übungsblatt 02
• Übungsblatt 03
• Übungsblatt 04
• Übungsblatt 05
• Übungsblatt 06

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
• Es wird ein ls14-scm Account unter Verwendung der @tu-dortmund.de Email Adresse benötigt
• Die gemeinsamen Ergebnisse des Praktikums werden im folgenden git Repository verwaltet: https://ls14-scm.cs.tu-dortmund.de/andrej.dudenhefner/lmse-ws1819.git
• 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

• Erstklausur: Mittwoch, der 13.02.2019 um 11:00 - 13:00 Uhr in HG1/HS6 (zusammen mit LMSE 2)
• Zweitklausur: Montag, der 18.03.2019 um 11:00 - 13:00 Uhr in HG1/HS6 (zusammen mit LMSE 2)

Klausurrelevante Themenbereiche

• Ungetypter lambda-Kalkül (beta-Reduktion, Normalisierung, Konfluenz, beta-Gleichheit, Kodierung)
• Einfach getypter lambda-Kalkül (Typableitung, Typinferenz, Inhabitation, Normalisierung)
• Curry-Howard Isomorphismus
• Intuitionistische Propositionallogik (Beweisbarkeit via Deduktion, Beweisbarkeit via Curry-Howard Isomorphismus, Widerlegbarkeit via Kripke-Struktur)