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

• Klaus Ostermann
  HeadKlaus Ostermann
• Philipp Schuster
  AlumniPhilipp Schuster

Klausur

Die Klausur findet am 16.02. von 10.15-11.45 Uhr im gewohnten Vorlesungsraum C215, Sand 14 statt.

Zeit und Ort

Vorlesung: Donnerstag, 10 c.t. bis 12 Uhr im Seminarraum C215, Sand 14.

Übung: Donnerstag, 12 s.t. bis 14 Uhr im Seminarraum C215, Sand 14.

Unterlagen

• SOS Coq Demo
• STLC
• Subtyping and System F
• Type Inference and Curry-Howard
• Featherweight Java
• Existential Types
• Higher-Order Types

Hausaufgaben

• Hausaufgabe 1
• Hausaufgabe 2
• Hausaufgabe 3
• Hausaufgabe 4
• Hausaufgabe 5
• Hausaufgabe 6
• Hausaufgabe 7 JavaExample HaskellExample
• Hausaufgabe 8 JavaExample HaskellExample
• Hausaufgabe 9
• Hausaufgabe 10 JavaExample HaskellExample
• Hausaufgabe 11
• Hausaufgabe 12

Zusatzmaterial

• Lösung 1
• Lösung 2
• Lösung 4
• Lösung 5

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.