Aktuelles.

• 11.06.2020: Ihr solltet alle eine E-Mail mit Anweisungen für die Klausur erhalten haben. Falls dies nicht der Fall ist, meldet euch bitte bei mir (christoph.stahl@tu-dortmund.de).
• 20.05.2020 UPDATE: Da ein Wechsel der Studierenden im Hörsaal nicht möglich ist, beginnt sowohl LMSE1 als auch LMSE2 um 9:30. Studierende, die nur eine der beiden Klausuren schreiben, verlassen dann um 10:30 den Hörsaal. Studierende, die beide Klausuren schreiben starten um 9:30 mit LMSE1 und wechseln um 10:30 auf LMSE2.
• 11.05.2020: Ein Termin für den Nachholtermin steht fest. Die Klausur (LMSE1) wird am 15.06.2020 um 9:30-10:30 stattfinden. Im Anschluss daran (Update: Parallel dazu) wird von 10:30-11:30 (Update: 9:30-10:30) die Klausur LMSE2 geschrieben. Alle Studierenden, die für den regulären Termin angemeldet waren, sollten automatisch für den Nachholtermin angemeldet sein, überprüft das aber bitte. Grundsätzlich wird es sich bei der Klausur um einen Freiversuch handeln, ein Nichtbestehen zählt somit nicht zu den drei möglichen Fehlversuchen. Sollten sich Studierende nachträglich für die Klausur anmelden wollen, schreibt uns bitte eine Email. Weitere Informationen gibt es auch hier auf der Fakultätsseite, sowie auf der Seite der Universität.
• 07.05.2020: Es gibt etwas Fortschritt bei der Planung zum Wiederholung der Klausuren. Noch gibt es keinen festen Termin, oder Ort, an dem unsere Klausur nachgeholt wird, aber es ist abzusehen, dass die Klausur in der Universität als Präsenzklausur stattfinden kann. Nach aktueller Planungsdiskussion könnte möglicherweise die Klausur im Juni nachgeholt werden. WICHTIG: Der aktuelle Planungsstand kann sich jederzeit ändern, sodass es nicht garantiert werden kann, dass eine Klausur im Juni durchgeführt werden kann. Sobald Termin und Ort feststeht, wird er an dieser Stelle verkündet.
  Es ist zur Zeit nicht geplant alternativ für alle eine mündliche Prüfung anzubieten. Falls ihr jedoch aus gesundheitlichen Gründen, oder aus Gründen der Gefährdung Anderer, oder aus Gründen, die euren Studienverlauf betreffen nicht an einer schriftlichen Klausur vor Ort teilnehmen könnt, könnt ihr euch bei uns melden, sodass wir für den Einzelfall eine Alternative finden können.
• 16.03.2020: Aufgrund der aktuellen Coronasituation wird die Nachklausur am 25.03.2020 nicht stattfinden. Zitat aus dem aktuellen Rundbrief der TU Dortmund: "Die TU Dortmund ist darum bemüht, etwaige nachteilige Folgen, die sich daraus für Studierende ergeben können, so gering wie möglich zu halten. Es wird nach möglichst frühen Nachholterminen gesucht. Optionen für digitale Alternativen werden geprüft.". Sobald wir mehr über das weitere Vorgehen wissen wird das an dieser Stelle veröffentlicht.
• 12.02.2020: Die erste Klausur ist korrigiert. Ergebnisse wurden ins Moodle hochgeladen. Die Einsicht ist am 28.02.2020 von 10-11 Uhr im OH12 2.013.
• 10.02.2020: Die Klausur am 12.02.2020 wird nur in HG II/HS 7 stattfinden. Damit die Klausur um 08:00 beginnen kann, seid bitte frühzeitig da. Einlass ist um 7:45.
• 29.01.2020: Die Studienleistung wird heute zusammen mit der LMSE2 Studienleistung eingetragen, da heute der Anmeldezeitraum für die Erstklausur abläuft, wird dieser um eine Woche verlängert. Sollte es zu Problemen kommen, schickt eine Email an christoph.stahl@tu-dortmund.de.
• 30.10.2019: Die Vorstellung der Projekte findet am Mittwoch, den 20.11.2019 anstelle der Vorlesung statt.
• 30.10.2019: Am Mittwoch, den 06.11.2019 fällt die Vorlesung wegen der Fachschafts Vollversammelung (FVV) aus.
• 14.10.2019: Tragt euch bis zum 18.10.2019 in das Wiki für eine Aufgabe ein. Pro Aufgabe sind maximal 3  Studierende vorgesehen, es gilt First Come First Serve.
• 07.10.2019: Die Uhrzeiten im AsSESS für den Dienstag waren fehlerhaft, diese sind nun korrigiert (Korrekt: Di 12:15-13:45). Bitte beachtet das!
• 07.10.2019: Erstellt euch einen Account im auf https://lmse.cs.tu-dortmund.de. Dies ist für das Praktikum erforderlich. Gebt danach an christoph.stahl@tu-dortmund.de bescheid, sodass ihr zum Praktikumsprojekt hinzugefügt werden könnt.
• 07.10.2019: Meldet Euch im Moodle Raum an. Dort werden Übungszettel und Vorlesungsfolien hochgeladen.
• 07.10.2019: Die Anmeldung im AsSESS werden Heute ab 12:00 freigeschaltet.
• Die Übungsanmeldung wird innerhalb der ersten Vorlesungswoche im AsSESS freigeschaltet. Die Anmeldefrist ist Freitag, der 11.10.2019 um 12:00 Uhr.

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.

• 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

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

Übungsgruppen

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: https://lmse.cs.tu-dortmund.de/christoph.stahl/lmse-ws1920
• 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 12.02.2020 um 8:00 - 10:00 Uhr in HG2/HS7 und MB/HS1 (zusammen mit LMSE 2)
• Zweitklausur: Montag, der 25.03.2020 um 8:00 - 10:00 Uhr in SRG1/H.001 (zusammen mit LMSE 2)