IMC011 Semantics and Domain Theory Spring 2012

Teacher

Herman Geuvers: home page

Introduction

Denotational Semantics is about assigning a mathematical meaning to syntax (in particular, that of programming languages) which is, in some sense, independent of how the syntax is presented, or what computational rules it may obey (which are properly the subject matter of Operational Semantics).

Domain Theory is the mathematics of the objects, sets-with-structure, and mappings between them, which serve as a vehicle for denotational semantics.

Material

  1. Lecture Notes on Denotational Semantics by Andy Pitts and Glynn Winskel, to be abbreviated to DENS for now. (Available via internet: PDF file)
  2. Selected sections (Ch. 3.1 and 3.2) from Domains and Lambda Calculi by Roberto Amadio and Pierre-Louis Curien, Cambridge University Press, 1998, pp: 484
  3. Selected sections (Ch. 13)from Formal Semantics of Programming Languages by Glynn Winskel, MIT Press, Cambridge, Massachusetts, 1993.
  4. Selected sections (Ch. 8)from Semantics of Programming Languages: Structures and Techniques, by Carl Gunter, MIT Press, Cambridge, Massachusetts, 1992.
Background material, notably on operational semantics can be found in Hanne Riis Nielson en Flemming Nielson: Semantics with applications, Wiley 1999 (now freely available).

Structure

The course is divided roughly into 3 parts:

Set up

The course consists of 2 hours combined "hoor-/werkcollege" TUESDAY, 15:45--17:30, in 5-7, 9-13, 16-17, 19-25 HG 01.057, plus "self study" and question time "on demand".

The course by week

The following gives a rough schedule.
  1. week 5: Chapter 1 of DENS, Exercises: see Blackboard
  2. week 6: Chapter 1 of DENS, Exercises:
    1. The two exercises of Winskel at the end of Chapter 1.
    2. Prove F(w_infty) = w_infty for F and w_infty in Winskel's notes
    3. Prove forall s exists n [F^n(bot)(s) = F^{n+1}(bot)(s)]
    4. Define a semantics for "repeat P until b"
    5. If you think "repeat" is easy, define a semantics for "for x = a to b do P". First try with a, b numbers, then think about the general situation, where a and b are arbitrary expressions.
  3. week 7: Chapter 2 of DENS
  4. week 9: Chapter 3 of DENS
  5. week 10: Chapter 4 of DENS.
  6. week 11: Chapter 5 of DENS
  7. week 12: Chapter 5 of DENS
  8. week 13: Chapter 6 of DENS
  9. week 16: Chapter 7 of DENS
  10. week 17: Chapter 8 of DENS
  11. week 19: Recap of DENS
  12. week 20: NO LECTURE
  13. week 21: Chapter 3.1 of Amadio-Curien
  14. week 22: Chapter 3.2 of Amadio-Curien
  15. week 23: Chapter 13 of Winskel-MIT
  16. week 24: Chapter 8 of Gunter-MIT and hand out of test exam
  17. week 25: Recap of part 2, questions on test exam

Exam

Tuesday 15:30 -- 17:30, week 26, HG 00.310, written exam.

Links


herman at cs dot ru dot nl