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
