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.
  • 27.6.2017: Einige Kleinigkeiten verbessert (Schreibfehler, etc.).
  • 24.7.2017: Noch mehr Kleinigkeiten verbessert.

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
  • 30.5.2017: Bis Ende Kapitel 6.5 (Prozeduren)
  • 13.6.2017: Bis Ende Kapitel 6 (Erweiterungen für While)
  • 20.6.2017: Bis Mitte Kapitel 7.2 (Fixpunkttheorie, Definition von oberen Schranken)
  • 27.6.2017: Bis Ende Kapitel 7.3 (Existenz des Fixpunkts für while)
  • 4.7.2017: Bis Anfang Kapitel 7.5 (Continuation-style denotationale Semantik, Definition von 𝒞⟦_⟧)
  • 11.7.2017: Bis Ende Kapitel 8.1 (Ein Korrektheitsbeweis mit der Denotationalen Semantik)
  • 18.7.2017: Bis Ende Kapitel 8.6 (Semantische Prädikate und syntaktische Bedingungen)
  • 25.7.2017: Bis Ende Kapitel 8 (Axiomatische Semantik)

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.

Änderungen

  • 16.6.2017: Beispiellösung Blatt 7 um eine vollständige Smallstep-Semantik für Parameterübergabe ergänzt.

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
30.05.2017 Sheet 7 - Procedures Download
13.06.2017 Sheet 8 - Type safety Download
20.06.2017 Sheet 9 - Denotational semantics Download
27.06.2017 Sheet 10 - Theory of fixed points Download
04.07.2017 Sheet 11 - Contexts Download
11.07.2017 Sheet 12 - Continuations Download
18.07.2017 Sheet 13 - Axiomatic Semantics 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
29.05.2017 Sample Solution Sheet 5 - Compiler Download
06.06.2017 Sample Solution Sheet 6 - Extensions of While Download
12.06.2017 Sample Solution Sheet 7 - Procedures Download
19.06.2017 Sample Solution Sheet 8 - Type safety Download
26.06.2017 Sample Solution Sheet 9 - Denotational semantics Download
03.07.2017 Sample Solution Sheet 10 - Theory of fixed points Download
10.07.2017 Sample Solution Sheet 11 - Contexts Download
17.07.2017 Sample Solution Sheet 12 - Continuations Download
24.07.2017 Sample Solution Sheet 13 - Axiomatic 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