Course Setup and Content

The course consists of lectures, problem assignments, programming assignments, and a research project. Via the problem assignments, you will deepen your understanding of the theoretical course material. Through the programming assignments, you will deepen your knowledge about program semantics, learn how it can lead directly to an implementation, and develop familiarity with the programming language Haskell. In the research project, you will study a complementary topic by reading a scientific publication, summarising the publication in an essay, and adding a contribution that relates the publication to the course material. You will present your summary and contribution in a short presentation to your peers.

We study models and meaning, the semantics, of computations and programming languages – the mathematics of computation and programming.

At the end of the course, you are able to:

• reason about various models of computation including functional, order-theoretic (complete lattices and domains), syntactic, and probabilistic models;
• explain the relation between the operational and denotational semantics of programming languages;
• formulate the semantics of imperative, functional, and probabilistic languages;
• design correct-by-construction programs using type systems;
• reason about computational models and semantics using concepts from category theory;
• explain how properties of programs can be formally proven;
• assess and communicate literature on the semantics of programming languages;
• write programs involving recursive data types and side effects in Haskell.

The course is based on lecture notes, of which you can find the most recent version in the release section of the gitlab project.

Prerequisites

We assume that you have some basic knowledge of

• Maps f : X → Y between sets and operations on sets (powerset, products, unions)
• Induction, at least on the natural numbers but even better structural induction;
• Context-free grammars (CFG) to generate formal languages;
• Logic (mainly deduction systems); and
• Programming.

You can consult the lecture notes of the logic course to refresh your memory.

Organisation

What will we be doing in the course? There are weekly lectures, see the schedule below, and you will have work yourself on the following things.

• Weekly assignments to work on during the tutorials
• Two larger theoretical problems, for which you have to submit worked-out solutions
• Three programming assignments (to worked on in pairs)
• A written essay that summarises and expands on a paper of your choice
• A final presentation of the findings from your essay

Submission Deadlines

The following is an overview over all the submission deadlines in chronological order. You may find detailed information for each part below.

1. Problem on lectures 1 - 3: Monday, 29 September, 23:59
2. Implementation of Arith semantics: Monday, 06 October, 23:59
3. Implementation of IMP semantics: Monday, 17 November, 23:59
4. Draft essay: Monday, 10 November, 23:59
5. Problem on lectures 4 - 9: Monday, 10 November, 23:59
6. Final essay: Monday, 08 December, 23:59
7. Implementation of λY semantics: Monday, 08 December, 23:59
8. Final presentation: Tuesday, 09 December, 09:00

Grading

The final grade is calculated as follows:

1. Programming exercises: 30% (group grade)
2. Problems: 20% (individual)
3. Written essay: 40% (individual)
4. Presentation: 10% (individual)

To pass the course, each individual grade has to be at least 5.5. Each component can be improved to obtain a passing grade by implementing the feedback that is provided if a reasonable attempt has been submitted for the original deadline.

What you will work on

Tutorials

There will be theoretical exercises provided throughout the course, which prepare you to work on the problems, the paper and your essay. It is expected that you work on these for the corresponding exercise session, even though the exercises are not mandatory. During the tutorial, we will interactively go through the solutions to these exercises.

Problems

We will distribute two theoretical problems, which are more involved than the exercises. You will have to submit individual solutions to these problems and you will receive feedback and a grade from us. You may discuss with others, but you need to understand and work out the solutions yourself. We may carry out random checks in form of a short oral examination to see that you understand the approach. By working out these problems, you will practise your writing and formal reasoning skills. The deadlines are as follows.

1. One problem on lectures 1 - 3: Monday, 29 September, 23:59
2. Feedback provided on first problem: Monday, 06 October
3. One problem on lectures 4 - 9: Monday, 10 November, 23:59
4. Feedback provided on second problem: Monday, 17 November

Programming Assignments

You will have to carry out three programming projects in pairs. The templates can be found on bitbucket. These templates may be updated throughout the course, but you will find the correct template attached as zip-file to the corresponding assignment.

Please form pairs for these exercises in the first week on Brightspace.

1. Semantics of Arith (Deadline: Monday, 06 October, 23:59)
2. Semantics of IMP (Deadline: Monday, 17 November, 23:59)
3. Semantics of λY (Deadline: Monday, 08 December, 23:59)

Written Essay

You have to pick a paper the list that will be provided, study this paper and summarise in a written essay. This essay needs to demonstrate that you have understood the paper and it needs to place the paper in the context of the course by stating and proving a theorem. The template and detailed evaluation criteria can be found in the Brightspace rubric attached to the assignment.

You will receive feedback on a first draft and then you have to submit the final version that will be evaluated. The timeline is as follows.

1. Picking of paper preferences: Friday, 03 October, 23:59
2. Assignment of paper: Monday, 06 October
3. Draft essay deadline (contains outline of essay and the theorem ): Monday, 10 November, 23:59
4. Draft feedback provided: Monday, 17 November
5. Final essay deadline: Monday, 08 December, 23:59
6. Final presentation: Tuesday, 09 December, 09:00 (tentative)
7. Essay mark provided: Monday, 15 December

Presentation

You will share your insights into the paper in a short presentation at the end of the course. We will discuss the dates together.

Lecture Schedule

We have every week a lecture at 9:00 and a tutorial at 11:00. Both take place in Gorleaus BW.0.31.

Here is the timetable of the course, numbered by week:

1. Tuesday, 02 September, 09:00: Lecture and tutorial 1 (HB)
2. Tuesday, 09 September, 09:00: Lecture and tutorial 2 (HB)
3. Tuesday, 16 September, 09:00: Lecture and tutorial 3 (HB)
4. Tuesday, 23 September, 09:00: Lecture and tutorial 4 (CF)
5. Tuesday, 30 September, 09:00: Lecture and tutorial 5 (CF)
6. Tuesday, 07 October, 09:00: Lecture and tutorial 6 (CF)
7. Tuesday, 14 October, 09:00: Lecture and tutorial 7 (CF)
8. Tuesday, 21 October, 09:00: Lecture and tutorial 8 (CF)
9. Tuesday, 28 October, 09:00: Lecture and tutorial 9 (HB)
10. Tuesday, 04 November, 09:00: Lecture and tutorial 10 (HB)
11. Tuesday, 11 November, 09:00: Lecture and tutorial 11 (HB)
12. Tuesday, 18 November, 09:00: Lecture and tutorial 12 (CF)
13. Tuesday, 25 November, 09:00: Lecture and tutorial 13 (HB)
14. Tuesday, 02 December, 09:00: Nothing
15. Tuesday, 09 December, 09:00: Final presentation session (until 15:00, depending on number of course participants)

Lecture and Tutorial 1

• Lecture: We discuss the course organisation, and will get a general overview over program semantics by looking at the ideas of programming languages and semantics in the case of the language Arith of simple arithmetic expressions.
• Tutorial: Pen-and paper exercises on Arith; Introduction to thinking in Haskell

Lecture and Tutorial 2

• Lecture: Mapping properties, categories and functors
• Tutorial: Pen-and paper exercises on categories and functors

Lecture and Tutorial 3

• Lecture: Syntactic contexts and classifying categories; functorial semantics; using natural transformations to relate semantics
• Tutorial: Pen-and paper exercises on functorial semantics and natural transformations

Lecture and Tutorial 4

• Lecture: the language IMP of simple imperative programs together with its big-step semantics
• Tutorial: Pen-and paper exercises on Imp; Haskell if needed

Lecture and Tutorial 5

• Lecture: We discuss partially ordered sets (posets) and their role in denotational semantics. Moreover, we introduce minima in posets, monotone maps and different categories with posets as objects.
• Tutorial: Pen-and paper exercises on big-step semantics of IMP; Haskell if needed

Lecture and Tutorial 6

• Lecture: In this second part on domain theory, we discuss approximations of program semantics via ω-chains in posets, suprema, ω-complete partial orders (ωcpos) and continuous maps with the goal of constructing fixed points that underlie the denotational semantics of languages like IMP.
• Tutorial: Pen-and paper exercises on fixed points and ωCPOs

Lecture and Tutorial 7

• Lecture: Program contexts for IMP, closure properties of continuous maps, the unique mapping property of products, and denotational semantics of arithmetic and Boolean expressions of IMP.
• Tutorial: Pen-and paper exercises on continuous maps and IMP OS

Lecture and Tutorial 8

• Lecture: Specific maps on ω-CPOs to handle memory, continuous maps on product ω-CPOs, continuity of basic IMP maps (if-then-else etc.), fixed points of (bi)continuous maps, and denotational semantics of IMP commands
• Tutorial: Pen-and paper exercises on command interpretations over ωCPOs

Lecture and Tutorial 9

• Lecture: Relation of denotational semantics of IMP to the operational semantics and contextual equivalence; isomorphisms of functors
• Tutorial: Pen-and paper exercises on IMP models

Lecture and Tutorial 10

• Lecture: Adjunctions between categories; terminal objects and Cartesian closed categories
• Tutorial: Pen-and paper exercises on adjunctions

Lecture and Tutorial 11

• Lecture: Syntax and type system of λY; substitution; big-Step operational semantics
• Tutorial: Pen-and paper exercises syntax and operational semantics of λY

Lecture and Tutorial 12

• Lecture: Contextual equivalence for λY, quotient categories, full and faithful functor, and defining good denotational semantics for λY
• Tutorial: Pen-and paper exercises on contextual equivalence for λY

Lecture and Tutorial 13

• Lecture: Denotational Semantics of λY; logical relations to prove adequacy; and failure of full abstraction
• Tutorial: Pen-and paper exercises on denotational semantics for λY