HOME | DEUTSCH | IMPRESSUM | KIT

Semantics of programming languages

Description only available in german.

Script

Das Semantik-Skript wurde von Andreas Lochbihler erstellt, im SS 2015 von Joachim Breitner ergänzt, und wird von uns weiter überarbeitet. Größere Änderungen werden hier erwähnt. Darüber hinaus wird angegeben, wie weit wir jeweils in der Vorlesung gekommen sind.

Änderungen

  • 24.4.2017: aktualisiertes Skript hochgeladen.
  • 9.5.2017: Kapitel "Mathematische Grundlagen" hinzugefügt.

Vorlesungsfortschritt

  • 24.4.2017: Bis einschließlich Abschnitt 2.1 (Syntax von While)
  • 25.4.2017: Bis zur Formulierung von Theorem 2 (Determinismus)
  • 2.5.2017: Bis Ende Kapitel 3.3
  • 9.5.2017: Bis Ende Kapitel 4.2 (Definition Compiler)
  • 16.5.2017: Bis Ende Kapitel 4
  • 23.5.2017: Bis zur Big-Step-Semantik für WhileX

Exercises

Parallel dazu gibt es eine Übung, in der die Inhalte der Vorlesung angewandt und vertieft werden. Dazu erscheint jede Woche ein Übungsblatt mit Aufgaben, die z.T. selbstständig, z.T. gemeinsam in der Übung gelöst werden. Im Anschluss wird hier eine Beispiellösung veröffentlicht.

Exercise sheets

Exercise sheets PDF
24.04.2017 Sheet 1 - Induction Download
25.04.2017 Sheet 2 - big step semantics Download
02.05.2017 Sheet 3 - small step semantics Download
09.05.2017 Sheet 4 - big and small step semantics Download
16.05.2017 Sheet 5 - Compiler Download
23.05.2017 Sheet 6 - Extensions of While Download
Sample Solutions PDF
05.04.2017 Sample Solution Sheet 1 - Induction Download
08.05.2017 Sample Solution Sheet 2 - big step semantics Download
15.05.2017 Sample Solution Sheet 3 - small step semantics Download
22.05.2017 Sample Solution Sheet 4 - big and small step semantics Download
Exercise sheets Sourcecode
25.04.2017 Derivation Trees in Prolog Download
25.04.2017 Evaluation of expressions in Prolog Download
Sample Solutions Sourcecode
08.05.2017 Implementation of Bigstep in Prolog Download

Schedule

Lecture:

begin 24.04.2017, end 29.07.2017

Weekday Begin End Location
Monday, 24.4.2017 9:45h 11:15h SR -118, Geb. 50.34
Tuesday 11:30h 13:00h SR 301, Geb. 50.34

Exercises:

begin 08.05.2017, end 29.07.2017

Weekday Begin End Location
Monday 9:45h 11:15h SR -118, Geb. 50.34
Tuesday, 6.6.2017 11:30h 13:00h SR 301, Geb. 50.34

Literature

  • Hanne Riis Nielson, Flemming Nielson. Semantics with Applications: An Appetizer. Springer Verlag, 2007. Zweite Auflage. ISBN: 978-1-84628-691-9.
    Grundlage der meisten Themen der Vorlesung, sehr anschaulich und gut verständlich.
  • John C. Reynolds. Theories of Programming Languages. Cambridge University Press, 1998. ISBN: 0-521-59414-6.
    Fokus auf denotationaler Semantik
  • Benjamin C. Pierce. Types and Programming Languages. MIT Press, 2002. ISBN: 0-262-162209-1.
    Schwerpunkt auf dem Lamda-Kalkül und Typsystemen, mit sehr guten Erklärungen, auch zu weiterführenden Themen.
  • Glynn Winskel. The Formal Semantics of Programming Languages. An Introduction. MIT Press, 1993. ISBN: 0-262-73103-7.
    Ausführlicher Beweis der Unentscheidbarkeit eines vollständigen axiomatischen Kalküls
  • Tobias Nipkow, Gerwin Klein. Concrete Semantics. Springer, 2014. ISBN: 978-3-319-10542-0. http://www.concrete-semantics.org/ Formalisierung des Vorlesungsstoffs im Theorembeweiser Isabelle, inklusive einer Einführung in diesen.

Personnel

Scientific Staff
Denis Lohner
Sebastian Ullrich