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 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
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.
Please form pairs for these exercises in the first week.
- Semantics of Simp (Deadline: Friday, 07 October, 23:59)
- Semantics of IMP (Deadline: Friday, 04 November, 23:59)
- Semantics of HOFL (Deadline: Friday, 02 December, 23:59)
- 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.
You will share your insights into the paper in a short presentation at the end of the course. We will discuss the dates together.
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:
- Tuesday, 06 September, 11:00: Lecture
- Tuesday, 13 September, 09:00: Lecture, but no practical this day
- Tuesday, 20 September, 09:00: Practical and Lecture at 11:00
- Tuesday, 27 September, 09:00: Practical and Lecture at 11:00
- Tuesday, 04 October, 09:00: Practical and Lecture at 11:00
- Tuesday, 11 October: No lecture and practical this day
- Tuesday, 18 October, 09:00: Practical and Lecture at 11:00
- Tuesday, 25 October, 09:00: Practical and Lecture at 11:00
- Tuesday, 01 November, 09:00: Practical and Lecture at 11:00
- Tuesday, 08 November, 09:00: Practical and Lecture at 11:00
- Tuesday, 15 November, 09:00: Practical and Lecture at 11:00
- Tuesday, 22 November, 09:00: Practical and Lecture at 11:00
- Tuesday, 29 November, 09:00: Practical and Lecture at 11:00
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.
Lecture: Categories and Functors
- Mapping Properties
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.
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.
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.
No practical session and lecture this week.
Lecture: Elements of Domain Theory III – Continuous Maps and Liftings
We finish the discussion of fixed points of continuous maps.
Lecture: Denotational Semantics of IMP
- Fixed points in CPOs
- Denotational Semantics of IMP
Lecture: Completeness for IMP and Higher-Order Functional Programming
- Completeness of contextual equivalence for denotational semantics in IMP
- Syntax HOFL
Lecture: Small-Step Operational Semantics of HOFL
- Free variables
- Small-step operational semantics
Lecture: Big-Step Operational Semantics and Contextual Equivalence of HOFL
Lecture: Denotational Semantics of HOFL
Lecture: Probabilistic Programming
- The language pIMP
- Big-step sampling semantics
- Some measure theory (measure spaces, probability measures, random variables)
- Sampling semantics as random variable