IMC011 Semantics and Domain Theory, Fall 2025

Teachers

Herman Geuvers: home page
Niels van der Weide: 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 Andrew Pitts, Glynn Winskel and Marcelo Fiore, abbreviated to DENS for now. (Available via internet: PDF file)
  2. Notes on dI domains , my notes for lectures 10, 11
  3. Models of untyped lambda calculus, my notes for the last 3 lectures, 12, 13, 14.
  4. Exercises for the exercises classes will appear on this webpage on a weekly basis.
  5. Answers to the exercises will appear on brightspace on a weekly basis.

Fresh up material for those who haven't followed Semantiek and Correctness or Semantics and Rewriting or have forgotten some of that:

  1. Material on operational semantics of While (called IMP by Pitts et al.) can be found in Hanne Riis Nielson en Flemming Nielson: Semantics with applications, Wiley 1999 (freely available). If you haven't done "Semantics and Correctness NWI-IBC026", read sections 1.2, 1.3, 2.1, 2.2.
  2. For a recap of lambda calculus, here is a set of selected pages from Introduction to Lambda Calculus by Barendregt and Barendsen. As exercises you may try 2.5 -- 2.10. If you haven't done Semantics and Rewriting NWI-IBC025, please study these notes.

Further reading material:

  1. Ch. 3.1 and 3.2 of Domains and Lambda Calculi by Roberto Amadio and Pierre-Louis Curien, Cambridge University Press, 1998, pp: 484
  2. Ch. 13 of Formal Semantics of Programming Languages by Glynn Winskel, MIT Press, Cambridge, Massachusetts, 1993.
  3. Ch. 2 and Ch. 8 until page 260 of Semantics of Programming Languages: Structures and Techniques, by Carl Gunter, MIT Press, Cambridge, Massachusetts, 1992.
  4. From computation to foundations via functions and application: The lambda-calculus and its webbed models, by Chantal Berline, Theoretical Computer Science 249 (2000) pp. 81-161.

Structure

The course is divided roughly into 3 parts:

Examination

There is a written exam, which is "open book", so you can take the course notes and your own notes to the exam. Apart from that there is a small assignment, see below.

The final grade is 3/4 of your written exam grade + 1/4 of your assignment grade.

Set up

The course consists of 2 hours hoorcollege Tuesday, 8:30--10:15 in HFML0220, plus "self study" and a "werkcollege" (exercise class) on Wednesday, 15:30-17:15 in HG01.028.

The course by week

The following is the preliminary weekly schedule (subject to change). See the schedule (rooster) and read the brightspace mails for the most up to date information.
Year-week Order Date Material Exercises, discussed on:
36 1 2/9 Slides and Section 1.1 of DENS exercises, 10/9
37 2 9/9 Section 1.2 of DENS and recap of Operational Semantics of "While" exercises, 17/9
38 3 16/9 Sections 2.1, 2.3, 3.1 of DENS (skip 2.2, slide 27 and 2.4) exercises, 24/9
39 4 23/9 Sections 2.2, 2.4, 3.2 of DENS exercises, 1/10
40 5 30/9 Sections 3.3, 4.1, 4.2 of DENS exercises, 8/10
41 6 7/10 Sections 4.3, 5.1, 5.2, 5.3 of DENS exercises, 15/10
42 7 14/10 in HG00.310 Sections 5.4, 5.5, 5.6 of DENS + presentation of the assignment exercises, 5/11
43 No lecture, autumn break
44 No lecture, autumn break
45 8 4/11 Chapter 6 of DENS exercises, 12/11
46 9 11/11 Chapter 7 of DENS exercises, 19/11
47 10 18/11 Chapter 8 of DENS and Notes on dI domains first part exercises 1--5, 26/11
48 11 25/11 Notes on dI domains continued exercises 6--11, 3/12
49 12 2/12 Short lambda calculus recap and Models of untyped lambda calculus, Section 1 and Section 2.1 exercises, 10/12
(If lambda calculus is new: read the Introduction to Lambda Calculus and try ex. 2.5 -- 2.10. For a lambda calculus "fresh up": read the first 4 pages of Models of untyped lambda calculus and do Exercises 1.7, 1.8, 1.9.)
50 13 9/12 Models of untyped lambda calculus, Section 2.2, Section 2.3 and Example 3.1 exercises, 17/12
51 14 16/12 Models of untyped lambda calculus, Section 3 exercises
3 16/1, 12:45-15:45 EXAM

Written Exam

The written exam is "open book", so you can take the course notes and your own notes to the exam. Dates:

Assignment

The deadline for the assignment is January 20. The resit deadline for the assignment is April 8.
In the assignment, you are requested to apply your knowledge on denotational semantics to a concrete programming language or programming concept (of your own choice). This should result in a short note (max 10 pages). See the assignment explanation. Your work should be sent to the teacher via mail, as a pdf file. You can do the assignment in couples; please write clearly on the title page the names and student numbers of the authors of the assignment.

herman at cs dot ru dot nl