Computational Models and Semantics, Autumn 2024
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
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
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 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 exercise classes
- Larger theoretical problems, out of which you have to submit worked-out solutions
- Three programming assignments
- 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.
- One problem from lectures 1 - 3 (as pair): Monday, 30 September, 23:59
- Implementation of Arith semantics: Monday, 07 October, 23:59
- Implementation of IMP semantics: Monday, 18 November, 23:59
- Draft essay: Monday, 11 November, 23:59
- One problem from lectures 4 - 9 (individually): Monday, 18 November, 23:59
- Draft feedback provided: Monday, 18 November
- Final essay: Monday, 09 December, 23:59
- Implementation of λY semantics: Monday, 09 December, 23:59
- Final presentation: Tuesday, 10 December, 09:00 (tentative)
Grading
The final grade is calculated as follows:
- Programming assignments: 40% (group grade)
- Written essay: 50% (individual)
- 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.
The two problems, which you work out and submit, are not part of the grade but we will provide feedback on them. This will greatly help you preparing for the essay and to deepen your understanding.
What you will work on
Exercise Classes
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.
Problems
We will distribute two theoretical problems per week, which are more involved than the exercises. You are encouraged to work on these to deepen your understanding. Throughout the course, you will pick two problems that you submit to receive feedback from us. One of these submissions will be as team of two, while the other is individual. By working out these problems, you will practise your writing and formal reasoning skills. The deadlines are as follows.
- One problem from lectures 1 - 3 (as pair): Monday, 30 September, 23:59
- Feedback provided on first problem: Friday, 04 October
- One problem from lectures 4 - 9 (individually): Monday, 18 November, 23:59
- Feedback provided on first problem: Friday, 22 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.
- Semantics of Arith (Deadline: Monday, 07 October, 23:59)
- Semantics of IMP (Deadline: Monday, 18 November, 23:59)
- Semantics of λY (Deadline: Monday, 09 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.
- Picking of paper preferences: Friday, 11 October, 23:59
- Assignment of paper: Monday, 14 October
- Draft essay deadline (draft contains outline of essay and narrative for positioning of the paper): Monday, 11 November, 23:59
- Draft feedback provided: Monday, 18 November
- Final essay deadline: Monday, 09 December, 23:59
- Final presentation: Tuesday, 10 December, 09:00 (tentative)
- Essay mark provided: Monday, 16 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 practical session at 11:00. Both take place in van Steenis, E0.03B.
Update from 24 September: We have every week a lecture at 9:00 and a practical session at 11:00. The lecture always takes place in Gorleaus DM 1.19, while the practical session changes room, see below.
Here is the timetable of the course, numbered by week:
- Tuesday, 03 September, 09:00: Lecture and practical 1 (HB)
- Tuesday, 10 September, 09:00: Lecture and practical 2 (CF)
- Tuesday, 17 September, 09:00: Lecture and practical 3 (CF)
- Tuesday, 24 September, 09:00: Lecture and practical 4 (HB) (practical in BW.0.31)
- Tuesday, 01 October: No lecture and practical this day
- Tuesday, 08 October, 09:00: Lecture and practical 5 (HB) (practical in BW.0.06)
- Tuesday, 15 October, 09:00: Lecture and practical 6 (CF) (practical Van Steenis - E0.03B, TBD)
- Tuesday, 22 October, 09:00: Lecture and practical 7 (CF) (practical in BW.0.06)
- Tuesday, 29 October, 09:00: Lecture and practical 8 (CF) (practical in BM 1.26)
- Tuesday, 05 November, 09:00: Lecture and practical 9 (HB) (practical in BW.0.06)
- Tuesday, 12 November, 09:00: Lecture and practical 10 (HB) (practical in BM.1.26)
- Tuesday, 19 November, 09:00: Lecture and practical 11 (HB) (practical in BM.1.26)
- Tuesday, 26 November, 09:00: Lecture and practical 12 (CF) (practical in BW.0.06)
- Tuesday, 03 December, 09:00: Lecture and practical 13 (HB) (practical in BM.1.26)
- Tuesday, 10 December, 09:00 (tentative): Final presentation session
Lecture and Practical 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.
- Practical Session: Introduction to thinking in Haskell and working on exercises for Arith.
Lecture and Practical 2
- Lecture: Mapping properties, categories and functors
- Practical Session: Pen-and paper exercises on categories, functors, and Arith
Lecture and Practical 3
- Lecture: Syntactic contexts and classifying categories; functorial semantics; using natural transformations to relate semantics
- Practical Session: Pen-and paper exercises on functorial semantics and natural transformations; Haskell if needed
Lecture and Practical 4
- Lecture: the language IMP of simple imperative programs together with its big-step semantics
- Practical Session: Pen-and paper exercises on Imp; Haskell if needed
Lecture and Practical 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.
- Practical Session: Pen-and paper exercises on big-step semantics of IMP; Haskell if needed
Lecture and Practical 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.
- Practical Session: Pen-and paper exercises on fixed points and ωCPOs
Lecture and Practical 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.
- Practical Session
Lecture and Practical 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
- Practical Session: Pen-and paper exercises on command interpretations over ωCPOs
Lecture and Practical 9
- Lecture: Relation of denotational semantics of IMP to the operational semantics and contextual equivalence; isomorphisms of functors
- Practical Session: Pen-and paper exercises on IMP models
Lecture and Practical 10
- Lecture: Adjunctions between categories; terminal objects and Cartesian closed categories
- Practical Session
Lecture and Practical 11
- Practical Session
- Lecture: Syntax and type system of λY; substitution; big-Step operational semantics
Lecture and Practical 12
- Lecture: Contextual equivalence for λY, quotient categories, full and faithful functor, and defining good denotational semantics for λY
- Practical Session
Lecture and Practical 13
- Lecture: Denotational Semantics of λY; logical relations to prove adequacy; and failure of full abstraction
- Practical Session