Computational Models and Semantics, Autumn 2022

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

Prerequisites

I assume that you have some basic knowledge of

  • Maps f : X → Y between sets (also called functions);
  • 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.

Programming Exercises

Please form pairs for these exercises in the first week.

  1. Semantics of Simp (Deadline: Friday, 07 October, 23:59)
  2. Semantics of IMP (Deadline: Friday, 04 November, 23:59)
  3. Semantics of HOFL (Deadline: Friday, 02 December, 23:59)
  4. Bonus: Implementation of derivation system

Self-Study and 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.

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 13 September and 11 October, we have every week a lecture at 11:00 and, from 20 September on, a practical session at 9:00. Both take place in Snellius 312.

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

  1. Tuesday, 06 September, 11:00: Lecture
  2. Tuesday, 13 September, 09:00: Lecture, but no practical this day
  3. Tuesday, 20 September, 09:00: Practical and Lecture at 11:00
  4. Tuesday, 27 September, 09:00: Practical and Lecture at 11:00
  5. Tuesday, 04 October, 09:00: Practical and Lecture at 11:00
  6. Tuesday, 11 October: No lecture and practical this day
  7. Tuesday, 18 October, 09:00: Practical and Lecture at 11:00
  8. Tuesday, 25 October, 09:00: Practical and Lecture at 11:00
  9. Tuesday, 01 November, 09:00: Practical and Lecture at 11:00
  10. Tuesday, 08 November, 09:00: Practical and Lecture at 11:00
  11. Tuesday, 15 November, 09:00: Practical and Lecture at 11:00
  12. Tuesday, 22 November, 09:00: Practical and Lecture at 11:00
  13. Tuesday, 29 November, 09:00: Practical and Lecture at 11:00

Week 1

Lecture: Organisation and Introduction

We discuss the general course organisation and will get a general overview over the course. Thereby we will get an idea of what programming languages and semantics are all about, and those ideas on the language Simp of simple arithmetic expressions.

Week 2

Lecture: Categories and Functors

  • Mapping Properties
  • Categories
  • Functors

Week 3

Practical: Introduction to Haskell

We will go together through some basics of Haskell and you can start working on the implementation of the semantics of Simp.

Lecture: The Language IMP of Imperative Programs and its Operational Semantics of IMP

The language IMP of simple imperative programs together with its big-step semantics will be introduced.

Week 4

Practical Session

Pen-and paper exercises on big-step semantics of IMP

Lecture: Elements of Domain Theory I – Posets, Bounds and Limits

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 5

Practical Session

Lecture: Elements of Domain Theory II – Monotone maps, directed sets, dcpos and continuity

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 6

No practical session and lecture this week.

Week 7

Practical Session

Lecture: Elements of Domain Theory III – Continuous Maps and Liftings

We finish the discussion of fixed points of continuous maps.

Week 8

Practical Session

Lecture: Denotational Semantics of IMP

  • Fixed points in CPOs
  • Denotational Semantics of IMP

Week 9

Practical Session

Lecture: Completeness for IMP and Higher-Order Functional Programming

  • Completeness of contextual equivalence for denotational semantics in IMP
  • Syntax HOFL

Week 10

Practical Session

Lecture: Small-Step Operational Semantics of HOFL

  • Free variables
  • Substitution
  • Small-step operational semantics

Week 11

Practical Session

Lecture: Big-Step Operational Semantics and Contextual Equivalence of HOFL

Week 12

Practical Session

Lecture: Denotational Semantics of HOFL

Week 13

Practical Session

Lecture: Probabilistic Programming

  • The language pIMP
  • Big-step sampling semantics
  • Some measure theory (measure spaces, probability measures, random variables)
  • Sampling semantics as random variable