IMC011 Semantics and Domain Theory, Fall 2019

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

Lecture Notes on Denotational Semantics by Andrew Pitts (and Glynn Winskel and Marcelo Fiore), abbreviated to DENS for now. (Available via internet: PDF file)
Grondslagen van de Informatica 2 course notes by Erik Barendsen, August 1988, abbreviated to GI2 for now
Selected sections from 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.

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

Material on operational semantics of While (called IMP by Pitts) 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.
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 "Berekeningsmodellen NWI-IBC025", please study these notes.

Further reading material:

Ch. 3.1 and 3.2 of Domains and Lambda Calculi by Roberto Amadio and Pierre-Louis Curien, Cambridge University Press, 1998, pp: 484
Ch. 13 of Formal Semantics of Programming Languages by Glynn Winskel, MIT Press, Cambridge, Massachusetts, 1993.
Ch. 2 and Ch. 8 until page 260 of Semantics of Programming Languages: Structures and Techniques, by Carl Gunter, MIT Press, Cambridge, Massachusetts, 1992.

Structure

The course is divided roughly into 3 parts:

Denotational Semantics of "While" and Domain Theory
Operational and Denotational Semantics of PCF
Models of the untyped lambda calculus

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, 10:30--12:15, plus "self study" and a "werkcollege" (exercise class) on Monday, 12:30-14:30 .

The course by week

The following is the weekly schedule. See the schedule (rooster) for the most up to date information on the lecture room.

Year-week	Order	Date and Location	Material	Exercises
36	1	3/9, HG02:032	Notes and Section 1.1 of DENS	exercises, 9/9, GR1.143 (Grotius Building), and some answers
37	2	10/9, HG00:086	Section 1.2 of DENS and recap of Operational Semantics of "While"	exercises, 16/9, GR1.143, and some answers
38	3	17/9, HG00:086	Sections 2.1, 2.3 of DENS (!skip 2.2 and slide 27 now!)	exercises, 23/9, GR1.143, and some answers
39	4	24/9, HG00:086	Sections 2.2, 2.4, 3.1, 3.2 of DENS	exercises, 30/9, GR1.143, and some answers
40	5	1/10, HG00:086	Sections 3.3, 4.1, 4.2 of DENS	exercises, 7/10, GR1.143, and some answers
41	6	8/10, HG00:086	Sections 4.3, 5.1, 5.2, 5.3 of DENS	exercises, 14/10, GR1.143, and some answers
42	7	15/10, HG00:086	Sections 5.4, 5.5, 5.6 of DENS + presentation of the assignment	exercises, 4/11, HG00.308, and some answers
43, 44			No lectures, autumn break
45	8	5/11, HG02.032	Chapter 6 of DENS	exercises, 11/11, HG00.308, and some answers
46	9	12/11, HG02.032	Chapter 7 of DENS	exercises, 18/11, HG01.028, and some answers
47	10	19/11, HG02.032	Chapter 8 of DENS and Stable models first part	exercises 1--4, 25/11, HG01.028, and some answers
48	11	26/11, HG02.032	Stable models continued	exercises 5--10, 2/12, HG00.308, and some answers
49	12	3/12, HG02.032	Lambda calculus recap and Models of lambda calculus: the notes of Berline	exercises, 9/12, HG00.308, and some answers
			(If lambda calculus is new: read the Introduction to Lambda Calculus and try ex. 2.5 -- 2.10.)
50	13	10/12, HG02.032	Sections 3.1, 3.2 and 3.3 of GI2	exercises, 16/12, HG00.308, and some answers
51	14	17/12, HG02.032	Chapter 4 of GI2	exercises, 22/1 13:30-15:15, HG01.028, and some answers
		22/1, 13:30-15:15, HG01.028	Question session and Exercises of week 14
4		23/1, 8:30-11:30, HG00.108	EXAM

Written Exam

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

Exam: 23/1, 8:30-11:30, HG00.108
Resit: 8/4, 8:30-11:30,, HG01.029, this will be an online with a possible short oral examination afterwards. See brightspace for details.
Here is a Test Exam and the handwritten answers to Test Exam.
Here is the June 2014 exam and the handwritten answers to it.

Assignment

The deadline for the assignment is January 23. The resit deadline for the assignment is April 9.
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