Semantics of Programming Languages

Fall 2004/05

Diplomstudiengang Informatik, Masterstudiengang Software Systems Engineering (Theoretical CS, Specialization Subject)

News

26.01.2005

The tutorial on January 31st has to be moved from lecture hall AH II to 5052 (one of the seminar rooms between buildings E1 and E2).

11.01.2005

The lecture on January 25th has to be cancelled. Solutions to exercise sheet 7 should be directly delivered to Markus Schlütter.

28.10.2004

Exercise 7 on the 2nd sheet employs a notation which has not been defined so far: O[[c]] denotes the state transformation which is caused by the statement c, that is, the functional O is defined by

O[[c]](σ) = σ' iff ⟨c,σ⟩ -> σ'.

28.10.2004

Because of the "Fachschaftsvollversammlung", the lecture on November 2nd has to be cancelled. Thus the next lecture will be given on November 9th, after the tutorial on November 8th. Solutions to the exercises should be returned at the institute or directly to the assistant, Markus Schlütter.

Dates

Contents

• The denotational semantics, which defines the input/output relation of a program by means of structural induction,
• The operational semantics, which describes the execution behaviour of a program, and
• The axiomatic semantics, which supports the proof of program properties.

Slides

0. Organization
1. Introduction (no slides)
2. Syntax of WHILE
3. Operational Semantics of WHILE (no slides)
4. Denotational Semantics of WHILE
5. Equivalence of Operational and Denotational Semantics (no slides)
6. Axiomatic Semantics of WHILE
7. Outlook: Blocks and Procedures

Exercises

Literature

• Glynn Winskel: The Formal Semantics of Programming Languages
  The MIT Press, 1996