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.
| Tag | Datum | Beginn | Ende | Ort |
|---|
| Dienstag | 23.04.2019 | 15:45 | 17:15 | Raum 301 |
| Dienstag | 30.04.2019 | 15:45 | 17:15 | Raum 301 |
| Dienstag | 07.05.2019 | 15:45 | 17:15 | Raum 301 |
| Dienstag | 14.05.2019 | 15:45 | 17:15 | Raum 301 |
| Dienstag | 21.05.2019 | 15:45 | 17:15 | Raum 301 |
| Dienstag | 28.05.2019 | 15:45 | 17:15 | Raum 301 |
| Dienstag | 04.06.2019 | 15:45 | 17:15 | Raum 301 |
| Dienstag | 11.06.2019 | 15:45 | 17:15 | Raum 301 |
| Dienstag | 18.06.2019 | 15:45 | 17:15 | Raum 301 |
| Dienstag | 25.06.2019 | 15:45 | 17:15 | Raum 301 |
| Dienstag | 02.07.2019 | 15:45 | 17:15 | Raum 301 |
| Dienstag | 09.07.2019 | 15:45 | 17:15 | Raum 301 |
| Dienstag | 16.07.2019 | 15:45 | 17:15 | Raum 301 |
| Dienstag | 23.07.2019 | 15:45 | 17:15 | Raum 301 |
Exercises:
Die Übung findet immer montags um 14:00 im Seminarraum -118 statt. In der ersten Vorlesungswoche
und am Pfingstmontag ist keine Übung.
| Tag | Datum | Beginn | Ende | Ort |
|---|
| Montag | 29.04.2019 | 14:00 | 15:30 | Raum -118 |
| Montag | 06.05.2019 | 14:00 | 15:30 | Raum -118 |
| Montag | 13.05.2019 | 14:00 | 15:30 | Raum -118 |
| Montag | 20.05.2019 | 14:00 | 15:30 | Raum -118 |
| Montag | 27.05.2019 | 14:00 | 15:30 | Raum -118 |
| Montag | 03.06.2019 | 14:00 | 15:30 | Raum -118 |
| Montag | 17.06.2019 | 14:00 | 15:30 | Raum -118 |
| Montag | 24.06.2019 | 14:00 | 15:30 | Raum -118 |
| Montag | 01.07.2019 | 14:00 | 15:30 | Raum -118 |
| Montag | 08.07.2019 | 14:00 | 15:30 | Raum -118 |
| Montag | 15.07.2019 | 14:00 | 15:30 | Raum -118 |
| Montag | 22.07.2019 | 14:00 | 15:30 | Raum -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
