Computational Models and Semantics, Autumn 2023

Course Setup and Content

The course consists of weekly lectures, see schedule below, programming assignments, practical assignment, self-study with a written essay and a final presentation The practical assignments are pen-and-paper exercises and are meant for deepening the understanding of lecture content. Although they do not contribute to the grade, they will help you with the other assignments.

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

  • You get to know various computational models: functional, domain theoretic, probabilistic
  • You understand small-step operational, big-step operational and denotational semantics and their differences
  • You learn how to give semantics to various kinds of programming languages: imperative and functional
  • You learn how to use category theory as abstraction
  • You learn how to implement semantics in Haskell

I will try to keep up with writing lecture notes, but this is not guaranteed. So please make sure to come to the lectures! The released version of the lecture notes can be found in the release section of the gitlab project.

Prerequisites

I 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 my lecture notes of the logic course to help refreshing your memory.

For the final part on probabilistic programming, you will need to have some understanding of calculus.

Exercises

There will be theoretical exercises provided throughout the course. It is expected that you work on these for the corresponding exercise session, even though the exercises are not mandatory. However, these are essential to comprehend the course and to work on the programming and essay assignments.

Grading

The final grade is calculated as follows:

  1. Programming assignments: 40% (group grade)
  2. Written essay: 50% (individual)
  3. Presentation: 10% (individual)

To pass the course, each individual grade has to be at least 5.5. Each part can be improved to obtain a passing grade with the feedback that is provided.

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, 09 October, 23:59)
  2. Semantics of IMP (Deadline: Monday, 20 November, 23:59)
  3. Semantics of PCF (Deadline: Monday, 11 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. 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, 13 October, 23:59
  2. Assignment of paper: Monday, 16 October
  3. Draft essay deadline (draft contains outline of essay and narrative for positioning of the paper): Monday, 13 November, 23:59
  4. Draft feedback provided: Monday, 20 November
  5. Final essay deadline: Monday, 04 December, 23:59
  6. Essay mark provided: Monday, 18 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.

Course Schedule

Except for 03 October, we have every week a lecture at 11:00 and, from 12 September on, a practical session at 9:00. Both take place in Snellius 4.01.

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

  1. Tuesday, 05 September, 11:00: Lecture week 1, but no practical this day
  2. Tuesday, 12 September, 09:00: Practical and lecture week 2
  3. Tuesday, 19 September, 09:00: Practical and lecture week 3
  4. Tuesday, 26 September, 09:00: Practical and lecture week 4
  5. Tuesday, 03 October: No lecture and practical this day
  6. Tuesday, 10 October, 09:00: Practical and lecture week 5
  7. Tuesday, 17 October, 09:00: Practical and lecture week 6
  8. Tuesday, 24 October, 09:00: Practical and lecture week 7
  9. Tuesday, 31 October, 09:00: Practical and lecture week 8
  10. Tuesday, 07 November, 09:00: Practical and lecture week 9
  11. Tuesday, 14 November, 09:00: Practical and lecture week 10
  12. Tuesday, 21 November, 09:00: Practical and lecture week 11
  13. Tuesday, 28 November, 09:00: Practical and lecture week 12
  14. Tuesday, 05 December, 09:00: Practical and lecture week 13

Week 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.
  • Lecture notes: Chapter 1

Week 2

  • Practical Session: Pen-and paper exercises on Arith.
  • Lecture: Mapping properties, categories and functors

Week 3

  • Practical: We will go together through some basics of Haskell and you can start working on the implementation of the semantics of Arith.
  • Lecture: Syntactic contexts and classifying categories; functorial semantics; using natural transformations to relate semantics

Week 4

  • Practical Session: Pen-and paper exercises on categories, functors and natural transformations; Haskell if needed
  • Lecture: the language IMP of simple imperative programs together with its big-step semantics

Week 5

  • Practical Session: Pen-and paper exercises on big-step semantics of IMP; Haskell if needed
  • Lecture: We discuss partially ordered sets and their role in denotational semantics. Moreover, we introduce some general kinds of bounds and limits (least upper bounds) that will be later refined for providing semantics.

Week 6

  • Practical Session
  • Lecture: In this second part on domain theory, we discuss monotone maps, directed sets, directed-complete partial orders (dcpos) and continuous maps with the goal of constructing fixed points that underlie the denotational semantics of languages like IMP.

Week 7

  • Practical Session
  • Lecture: Program context for IMP, closure properties of continuous maps and adjunctions

Week 8

  • Practical Session
  • Lecture: Fixed points in CPOs and denotational semantics of IMP

Week 9

  • Practical Session
  • Lecture: Relation of denotational semantics of IMP to the operational semantics and contextual equivalence

Week 10

  • Practical Session
  • Lecture: Syntax and type system of PCF; substitution

Week 11

  • Practical Session
  • Lecture: Big-Step operational semantics and contextual equivalence for PCF

Week 12

  • Practical Session
  • Lecture: Denotational Semantics of PCF

Week 13

  • Either
    • Practical Session
    • Buffer in case we have to move a lecture due unforeseen circumstances
  • Or
    • Practical Session
    • Lecture: Probabilistic Programming and big-step sampling semantics. However, sampling semantics as random variable would require some measure theory (measure spaces, probability measures, random variables) and we will probably not have the time for that
  • Or: presentation session