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
| Former Staff Member |
|---|
| Dr.-Ing. Sebastian Ullrich |
| Dipl.-Inform. Denis Lohner |