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

  • 23.4.2019: Kapitel 1.3: Beispiel der operationalen Semantik an spätere Notation angepasst.
  • 3.5.2019: Ein Versuch, Variablen konsistenter von 1 ausgehend durchzuzählen
  • 21.5.2019: Prosa-Erklärung zum Aufteilungslemma hinzugefügt, JmpFT-Regel zu JmpTT umbenannt
  • 28.5.2019: Übungsaufgabe zu WhileBlock hinzugefügt
  • 4.6.2019: Syntax der BigStep-Semantik mit Prozeduren geändert: E jetzt rechts vom Turnstile
  • 9.7.2019: Variablen in Theorem 128 etwas sinnvoller benannt

Vorlesungsfortschritt

  • 23.4.2019: Bis einschließlich Abschnitt 3.1 (Syntax von While)
  • 30.4.2019: Bis zur Formulierung von Theorem 10 (Determinismus)
  • 7.5.2019: Bis einschließlich Lemma 19
  • 14.5.2019: Bis Ende Kapitel 5.2 (Definition Compiler)
  • 21.5.2019: Bis Ende Kapitel 5
  • 28.5.2019: Bis einschließlich Lemma 46
  • 5.6.2019: Bis Ende Kapitel 6.5 (Prozeduren)
  • 11.6.2019: Bis Ende Kapitel 6 (Erweiterungen für While)
  • 18.6.2019: Bis Mitte Kapitel 7.2 (Fixpunkttheorie, Definition von oberen Schranken)
  • 25.6.2019: Bis Ende Kapitel 7.2 (Knaster-Tarski-Fixpunktsatz)
  • 2.7.2019: Bis Ende Kapitel 7.4 (Bezug zur operationalen Semantik)
  • 9.7.2019: Bis Ende Kapitel 8.1 (Ein Korrektheitsbeweis mit der Denotationalen Semantik)
  • 16.7.2019: Bis Ende Kapitel 8.6 (Semantische Prädikate und syntaktische Bedingungen)
  • 23.7.2019: 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

  • 8.5.2019: Hinweis zu ÜB 3 Aufgabe 2 ergänzt, Blatt veröffentlicht.
  • 13.5.2019: Fehler in Aufgabe 1 auf Blatt 3 verbessert, Lösung veröffentlicht.

Exercise sheets

Exercise sheets Sourcecode
30.04.2019 common.pl Download
06.05.2019 bigstep.pl Download
06.05.2019 derivTree.pl Download
Exercise sheets PDF
26.04.2019 Sheet 1 - Induction Download
30.04.2019 Sheet 1 (Solution) - Induction Download
30.04.2019 Sheet 2 - Big-Step Download
06.05.2019 Sheet 2 (solution) - Big-Step Download
08.05.2019 Sheet 3 - Small-Step Download
13.05.2019 Sheet 3 (Solution) - Small-Step Download
16.05.2019 Sheet 4 - Big-Step and Small-Step Download
20.05.2019 Sheet 4 (Solution) - Big-Step and Small-Step Download
21.05.2019 Sheet 5 - Compiler Download
28.05.2019 Sheet 5 (Solution) - Compiler Download
28.05.2019 Sheet 6 - Extensions to the While language Download
03.06.2019 Sheet 6 (Solution) - Extensions to the While language Download
05.06.2019 Sheet 7 - Procedures Download
11.06.2019 Sheet 8 - Type safety Download
17.06.2019 Sheet 7 (Solution) - Procedures Download
17.06.2019 Sheet 8 (Solution) - Type safety Download
18.06.2019 Sheet 9 - Denotational Semantics Download
24.06.2019 Sheet 9 (Solution) - Denotational Semantics Download
25.06.2019 Sheet 10- Fixpoint Theory Download
02.07.2019 Sheet 10 (Solution) - Fixpoint Theory Download
02.07.2019 Sheet 11 - Contexts Download
09.07.2019 Sheet 11 (Solution) - Contexts Download
09.07.2019 Sheet 12 - Continuations Download
15.07.2019 Sheet 12 (Solution) - Continuations Download
22.07.2019 Sheet 13 - Axiomatic Semantics Download
22.07.2019 Sheet 13 (Solution) - Axiomatic Semantics Download

Schedule

Lecture:

Die Vorlesung findet immer dienstags um 15:45 im Seminarraum 301 statt.
TagDatumBeginnEndeOrt
Dienstag 23.04.201915:4517:15Raum 301
Dienstag 30.04.201915:4517:15Raum 301
Dienstag 07.05.201915:4517:15Raum 301
Dienstag 14.05.201915:4517:15Raum 301
Dienstag 21.05.201915:4517:15Raum 301
Dienstag 28.05.201915:4517:15Raum 301
Dienstag 04.06.201915:4517:15Raum 301
Dienstag 11.06.201915:4517:15Raum 301
Dienstag 18.06.201915:4517:15Raum 301
Dienstag 25.06.201915:4517:15Raum 301
Dienstag 02.07.201915:4517:15Raum 301
Dienstag 09.07.201915:4517:15Raum 301
Dienstag 16.07.201915:4517:15Raum 301
Dienstag 23.07.201915:4517:15Raum 301

Exercises:

Die Übung findet immer montags um 14:00 im Seminarraum -118 statt. In der ersten Vorlesungswoche und am Pfingstmontag ist keine Übung.
TagDatumBeginnEndeOrt
Montag 29.04.201914:0015:30Raum -118
Montag 06.05.201914:0015:30Raum -118
Montag 13.05.201914:0015:30Raum -118
Montag 20.05.201914:0015:30Raum -118
Montag 27.05.201914:0015:30Raum -118
Montag 03.06.201914:0015:30Raum -118
Montag 17.06.201914:0015:30Raum -118
Montag 24.06.201914:0015:30Raum -118
Montag 01.07.201914:0015:30Raum -118
Montag 08.07.201914:0015:30Raum -118
Montag 15.07.201914:0015:30Raum -118
Montag 22.07.201914:0015:30Raum -118

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

Department Head
Prof. Gregor Snelting
Scientific Staff
Sebastian Ullrich
Maximilian Wagner