Semantik von Programmiersprachen
Vorlesung, 4-std., Mo 12-14, Mi 10-12; Übung 2-std., Do 16-18; Abel, Schöpp
Aktuelles
- Die Prüfungen finden am 8. Oktober statt.
- Die Übung am 22.7. findet im Raum L109 statt.
Inhalt
Bei der Arbeit mit Programmiersprachen, zum Beispiel bei der Entwicklung von Compilern und Interpretern oder bei der Programmanalyse, ist es wichtig, dass die Bedeutung von Programmen (ihre Semantik) genau festgelegt ist. In dieser Vorlesung sollen Grundlagen der Semantik von Programmiersprachen vermittelt werden. Neben der reinen Spezifikation der Bedeutung von Programmen soll auf einige der vielfältigen Anwendungen semantischer Methoden eingegangen werden, zum Beispiel in der rechnergestützten Analyse und Verifikation von Programmen oder in der Entwicklung von Typsystemen.
- Einführung in operationelle, denotationelle und axiomatische Semantik am Beispiel einer einfachen imperativen Sprache
- Lambda-Kalkül mit einfachen Typen
- Operationelle und denotationelle Semantik einer funktionalen Programmiersprache (PCF)
- Algorithmische Spielsemantik
Organisation
- Umfang: 4+2 Semesterwochenstunden
- Vorlesung und Übungen: Dr. Andreas Abel, Dr. Ulrich Schöpp
- Zuordnung: T
Zeit und Ort
| Veranstaltung | Zeit | Ort | Beginn |
|---|---|---|---|
| Vorlesung | Mo, 12-14 Uhr | Raum 065 (Oettingenstr. 67) | 19.04.2010 |
| Vorlesung | Mi, 10-12 Uhr | Raum 065 (Oettingenstr. 67) | 21.04.2010 |
| Übung | Do, 16-18 Uhr | Raum 065 (Oettingenstr. 67) | 29.04.2010 |
Log
| Termin | Stoff | Sonstiges |
|---|---|---|
| 19.04. | Einführung und Überblick | |
| 21.04. | Syntax von IMP, SMC-Maschine, strukturelle Induktion | Übungsblatt 1 |
| 26.04. | Induktive Definitionen, Regelinduktion | |
| 28.04. | Small-Step-Semantik für IMP | Übungsblatt 2 |
| 03.05. | Big-Step-Semantik für IMP, Einige Spracherweiterungen | bigstep.hs, bigstep.ml |
| 05.05. | Denotationelle Semantik für IMP | Übungsblatt 3 |
| 10.05. | Grundbegriffe der Bereichstheorie | |
| 12.05. | Fortsetzung Bereichstheorie | Übungsblatt 4 |
| 17.05. | Axiomatische Semantik für IMP | |
| 19.05. | Lambda-Kalkül: Syntax, α-Äquivalenz | Übungsblatt 5 |
| 26.05. | β-Reduktion, lokale Konfluenz | Übungsblatt 6 |
| 31.05. | Konfluenz der beta-Reduktion | |
| 02.06. | Typzuweisung | Übungsblatt 7 |
| 07.06. | Getypte Gleicheit und Standardmodell | |
| 09.06. | Umgebungsmodelle | Übungsblatt 8 |
| 14.06. | Termmodelle und Normalisierung | |
| 16.06. | Logische Relationen und Vollständigkeit des Standardmodells | Übungsblatt 9 |
| 21.06. | Kategorien | |
| 23.06. | Kartesisch abgeschlossene Kategorien | Übungsblatt 10 |
| 28.06. | Lambda-Kalkül und CCCs | |
| 30.06. | Effekte im Lambda-Kalkül | Übungsblatt 11 |
| 05.07. | Effekte und Monaden | |
| 07.07. | PCF Syntax und Big-Step Semantik | Übungsblatt 12 |
| 12.07. | PCF Observationsäquivalenz und Kontextlemma | |
| 14.07. | CPO-Semantik für PCF | Übungsblatt 13 |
| 19.07. | PCF Interpretation, Adäquatheit | |
| 21.07. | Adäquatheit, Full Abstraction |
Literatur
Bücher
- Glynn Winskel, The Formal Semantics of Programming Languages, 1993
- Carl Gunter, Semantics of Programming Languages: Structures and Techniques, 1992
Weitere Artikel
- Gordon Plotkin, A Structural Approach to Operational Semantics (PostScript)
Klassischer Artikel über strukturelle operationelle Semantik. - Andrew Pitts, Lecture Notes on Semantics of Programming Languages
- Glynn Winskel, Lecture Notes on Denotational Semantics (PDF)
- Sandrine Blazy and Xavier Leroy. Mechanized semantics for the Clight subset of the C language
Beispiel einer operationellen Semantik für eine realistische Programmiersprache. Diese Semantik ist die Basis für den verifizierten CompCert-Compiler. - John Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures
Beispiel für die Benutzung von Hoare Logik zum Beweis von Eigenschaften von Programmen, in denen Zeigerarithmetik benutzt wird. - Luke Ong. Correspondence between Operational and Denotational Semantics (PS.GZ), In Handbook of Logic in Computer Science, Volume 4, 1995
Übersichtsartikel über PCF mit Beweisen für viele klassische Resultate.
Artikelaktionen