Vorlesung: Semantik von Programmiersprachen

Semester: Sommersemester 1995

Professor: Gert Smolka, Tel 5311

Assistent: Joachim Niehren, Tel 5330

Ort: Do, 11-13, HS I, Fr. 11-13, HS II, Geb. 27

Teilgebiet: Theoretische Informatik, Stammvorlesung

Vorkenntnisse: Vordiplom

Übungen: Di, 16-18, Zeichensaal, Geb. 27 und Mi 11-13, Seminarraum 1, Geb.27.

Voraussetzungen zur Scheinvergabe: Genügend Punkte bei den Übungen

Fortsetzungsveranstaltungen: keine

Zweck der Veranstaltung: Die Vorlesung führt grundlegende Techniken zur formalen Beschreibung der Semantik von Programmiersprachen ein. Dabei stehen denotationale und operationale Semantiken und deren Korrespondenzen im Vordergrund.

Behandelter Stoff: Wichtige Themen sind: imperative Sprachen, rekursive Definition von partiellen Funktionen, funtionale Sprachen höherer Ordnung, Fixpunktsemantiken, axiomatische Semantiken, Bereichstheorie und Typsysteme.

Vermittelte Fähigkeiten: Die in der Vorlesung vermittelten Techniken sollen den Studenten in die Lage versetzen, die Semantik von Programmiersprachen formal zu definieren und daraus Beweismethoden für die Eigenschaften von Programmen herzuleiten.
Die Vorlesung gibt auch eine kurze Einführung in die funktionale Programmiersprache SML, die für Programmierübungen verwendet wird.

Literatur: Die Vorlesung wird im wesentlichen nach dem Lehrbuch

Glynn Winskel
The Formal Semantics of Programming Languages.
The MIT Press, Cambridge, Massuchusetts, 1993.

gehalten.