Programmiersprachen II
In dieser Lehrveranstaltung untersuchen wir fortgeschrittene Konzepte von Programmiersprachen. Wir werden unterschiedliche Methoden kennenlernen, die Semantik von Programmiersprachen zu definieren (operationelle Semantik, denotationelle Semantik) und formal Eigenschaften von Programmiersprachen zu beweisen. Ein besonderer Schwerpunkt der Lehrveranstaltung ist die Definition und Analyse von statischen Typsystemen. Das Ziel dieser Lehrveranstaltung ist ein tieferes Verständnis von modernen Programmiersprachen und eine Vorbereitung darauf, aktuelle Forschungsarbeiten in dem Bereich zu verstehen.
Dozenten
Klausur
Die Klausur findet am 29.7. von 10.15-11.45 Uhr im Hörsaal Kriminologie (Raum F119, Sand 6) statt.
Die Ergebnisse der Klausur hängen jetzt aus (zwischen den Büros B214 und B215).
Klausureinsicht
Für die Klausureinsicht könnt Ihr am Mittwoch, dem 14. Oktober zwischen 14 und 16 Uhr bei Tillmann im Büro vorbeikommen (Sand, B213). Oder Ihr vereinbart einen anderen Termin per Email.
Nachprüfung
Die Nachprüfung wird als mündliche Prüfung stattfinden, vorraussichtlich in der zweiten Woche der Vorlesungszeit (19. bis
- Oktober). Bitte meldet Euch bei Tillmann per Email, wenn Ihr an der Nachprüfung teilnehmen wollt, dann vereinbaren wir einen Termin.
(Einige haben bereits mit Prof. Ostermann einen Termin vereinbart. Ihr braucht Euch nicht noch einmal anzumelden).
Zeit und Ort
Vorlesung: Donnerstag, 16 c.t. bis 18 Uhr im Hörsaal A301, Sand 1.
Übungsbetrieb
Wir bieten eine Übungsgruppe an. Die Teilnahme an den Übungsterminen ist freiwillig.
- Montags, 14:00 c.t. bis 16:00, im Hörsaal A301, Sand 1.
Es gibt keine besondere Anmeldung zum Übungsbetrieb. In den Übungen experimentieren wir in kleinen Gruppen mit den Methoden aus der Vorlesung. Bereits stattgefundene Übungen:
Structural induction on typing derivations. Read more …
Program in untyped lambda calculus and prove properties of lambda terms. Read more …
Beweisen Sie, daß die in der ersten Hausaufgabe zusätzlich eingeführten Regeln die Sprache nicht wirklich verändern. Read more …
Entwickeln Sie Syntax und Semantik einer ganz einfachen Sprache und beweisen Sie eine einfache Eigenschaft für alle Terme. Read more …
Hausaufgaben
Es wird wöchentliche Hausaufgaben geben, die als 20% in die Gesamtnote eingehen. Bisher gestellte Hausaufgaben mit ihren Abgabefristen:
Beschäftigen Sie sich mit parametrischer Polymorphie und der Curry-Howard-Korrespondenz. Read more …
Beschäftigen Sie sich mit der Verwendung und der Struktur der Relation T <: T aus der Vorlesung. Read more …
Learn to program in λ-calculus. Read more …
Beschäftigen Sie sich mit Progress und Preservation sowie der operationalen Semantik des ungetypten λ-Kalküls. Read more …
Beschäftigen Sie sich mit den t → t′ und t : T Relationen aus der Vorlesung. Read more …
Beweisen Sie eine Eigenschaft der Sequenz S0, S1, … aus der Vorlesung und fügen Sie der Semantik einer einfachen Sprache einige Regeln hinzu. Read more …
Unterlagen
Literaturempfehlung
- B.C. Pierce, Types and Programming Languages, MIT Press
- R. Harper, Practical Foundations for Programming Languages, Cambridge University Press, 2013. Eine kostenlose Online-Ausgabe findet sich auf der Homepage des Autors.