HOME | DEUTSCH | IMPRESSUM | KIT

Semantics of programming languages

Description only available in german.

Script

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

Änderungen

  • 17.3.2015: Skript hochgeladen.
  • 6.5.2015: Kleine Vereinfachung des Beweises des Aufteilungslemmas (Lemma 16).
  • 20.5.2015: Variation der Big-Step-Semantik für WhileX.
  • 16.7.2015: Ergänzung Bonuskapitel 8.
  • 16.7.2015: Beispiele und Definitionen werden jetzt wie gewünscht gemeinsam mit Lemmas und Theoremen hochgezählt.

Vorlesungsfortschritt

  • 13.4.2015: Bis einschließlich Abschnitt 2.1 (Syntax von While)
  • 15.4.2015: Bis zur Formulierung von Theorem 2 (Determinismus)
  • 22.4.2015: Bis zur Formulierung von Lemma 7 (Zerlegungslemma für Sequenz)
  • 29.4.2015: Bis zu Definition 11 (Compiler)
  • 6.5.2015: Bis Ende Kapitel 4
  • 13.5.2015: Bis zur Small-Step-Semantik für WhileX
  • 20.5.2015: Bis Ende Kapitel 5.5 (Prozeduren)
  • 27.5.2015: Bis einschließlich Lemma 24 (Erhalt der Zustandskonformanz)
  • 3.6.2015: Bis Ende Kapitel 6.1 (Definition der denotationalen Semantik)
  • 10.6.2015: Bis Ende Kapitel 6.2 (Fixpunkttheorie)
  • 17.6.2015: Bis Ende Kapitel 6.4 (Bezug zur Operationalen Semantik)
  • 24.6.2015: Bis Ende Kapitel 6 (Denotationale Semantik)
  • 1.7.2015: Bis Ende Kapitel 7.3 (Inferenzregeln für While)
  • 8.7.2015: Bis Ende Kapitel 7.6 (Semantische Prädikate und syntaktische Bedingungen)
  • 13.7.2015: Bis Ende Kapitel 7.7 (Verifikationsbedingungen)
  • 15.7.2015: Bonuskapitel 8 (Semantik von Funktionalen Programmiersprachen)

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. selbsständig, z.T. gemeinsam in der Übung gelöst werden. Im Anschluss wird hier eine Musterlösung veröffentlicht.

Exercise sheets

Exercise sheets PDF
13.04.2015 Sheet 1 - Induction Download
15.04.2015 Sheet 2 - big step semantics Download
22.04.2015 Sheet 3 - small step semantics Download
29.04.2015 Sheet 4 - big and small step semantics Download
06.05.2015 Sheet 5 - Compiler Download
13.05.2015 Sheet 6 - Extensions of While Download
20.05.2015 Sheet 7 - Procedures Download
27.05.2015 Sheet 8 - Type safety Download
03.06.2015 Sheet 9 - Denotational semantics Download
10.06.2015 Sheet 10 - Theory of fixed points Download
17.06.2015 Sheet 11 - Contexts Download
24.06.2015 Sheet 12 - Continuations Download
06.07.2015 Sheet 13 - Axiomatic Semantics Download
Exercise sheets Sourcecode
15.04.2015 Evaluation of expressions in Prolog Download
20.04.2015 Derivation Trees in Prolog Download

Schedule

Lecture:

begin 13.04.2015, end 15.07.2015

Weekday Begin End Location
Monday, 13.4.2015 9:45h 11:15h SR 236, Geb. 50.34
Wednesday 14:00h 15:30h SR 236, Geb. 50.34

Exercises:

begin 20.04.2015, end 13.07.2015

Weekday Begin End Location
Monday 9:45h 11:15h SR 236, 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

Personnel

Department Head
Prof. Gregor Snelting
Scientific Staff
Denis Lohner
Former Staff Member
Dr. rer. nat. Joachim Breitner