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.
• Die Abschlusspräsentation der Praktikumsprojekte findet am Mittwoch, dem 23.01.2019 an Stelle der Vorlesung statt. Mindestens ein Mitglied jeder Gruppe muss für die Vorstellung der Gruppenarbeit anwesend sein.
• In der Woche vom 14.01. bis zum 18.01. fällt die Vorlesung und Übungen aufgrund einer Dienstreise aus.
• Die Aufgabenverteilung des Praktikums befindet sich im Wiki
• Die Praktikumsanmeldung erfolgt we folgt
  • Bitte jeweils Nutzername/Email des Accounts bei https://ls14-scm.cs.tu-dortmund.de bis Freitag, den 30.11.2018 um 12:00 Uhr an Andrej Dudenhefner schicken, um einem Praktikumsprojekt zugeordnet zu werden
  • Teilen Sie ggf. mit, mit welchen Teilnehmern Sie gerne in einer Praktikumsgruppe sein möchten
  • Teilen Sie ggf. mit, welche Praktikumsaufgabe Sie gerne bearbeiten würden (letztendlich werden alle Aufgaben verteilt)
  • Eine Übersicht über die Aufgaben befindet sich hier
• Die Übungsanmeldung ist in AsSESS freigeschaltet. Die Anmeldefrist ist Freitag, der 30.11.2018 um 12:00 Uhr. Bitte stellen Sie sicher, dass Ihre Daten in AsSESS aktuell sind.

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.

• 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
• Principal Type-schemes for Functional Programs by Luis Damas and Robin Milner

Folien

• Kombinatorische Logik Synthese und das Intersektionstypsystem
• Subtyping, Refinement und CLS
• System F
• Starke Normalisierung von System F und der Hindley-Milner Kalkül
• Klassische Logik und der Curry-Howard Isomorphismus
• Lambda-Delta Kalkül
• Dependent Types - Definitionen
• Dependent Types - Entscheidungsprobleme
• Lambda Cube

Ü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

Übungszettel

• Ü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 Beweisaufgabe 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
• Aufgaben zu LMSE 2 befinden sich unter lmse-ws1819/lmse-2
• 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

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

Klausurrelevante Themenbereiche

• Reduktionsbegriffe (beta-Reduktion, call-by-name Reduktion, call-by-value Reduktion)
• Intersektionstypsystem (Typableitung, Typinferenz, Inhabitation)
• System F (Typableitung, Typinferenz, Inhabitation)
• Lambda-Delta-Kalkül (Typableitung, Typinferenz, Inhabitation)
• Klassische Propositionallogik (Einbettung in intuitionistische Propositionallogik, Beweisbarkeit via Deduktion, Beweisbarkeit via Curry-Howard Isomorphismus)