Principles of Programming Languages
- ÕIS data: LTAT.03.027, 6 ECTS.
- Lectures: TBA
- Exercise classes: TBA
- Lecture slides, exercise sheets, sample solutions, weekly info: Moodle
- Language English.
- Contact: Danel Ahman Danel Ahman
Course overview
As programs are getting easier to automatically generate (e.g., using various large language models), then it is becoming ever more important to understand what the generated code means, how it executes, what it can do, and how to formally reason about its correctness.
This course will give the students the required knowledge to be able to mathematically model their (generated) programs, formally reason about the behaviour and equivalence of such programs, and formulate, write, and verify the correctness properties of such programs (both in terms of functional correctness concerning the computed values but also in terms of the side-effects the programs might cause during their execution).
The course consists of three main parts:
In the first part, we recall and revisit the simply typed lambda calculus and other related calculi (as formal models underlying many modern programming languages), and discuss the operational and denotational semantics of such calculi, how they are related, and how to formally reason about them.
In the second part, we extend the simply typed lambda calculus with a wide variety of computational side-effects, study how to do this in a uniform and principled way, and study the computational behaviour of such extensions (e.g., by investigating the corresponding operational and denotational semantics).
In the third part, we will concentrate on reasoning about program correctness. We will then investigate type-and-effect systems, type-and-coeffect systems, and dependent types as a means to encode correctness specifications in types, and to verify them. To this end, we will explore both functional correctness properties, and properties concerning side-effects and their behaviour.
Weekly topics
(Changes in topics and their order are possible across the semester.)
- Introduction and untyped lambda calculus
- Simply typed lambda calculus
- Call-by-value/call-by-name small-step/big-step operational semantics
- Declarative and algorithmic subtyping
- Program equivalences and strong normalisation
- Denotational semantics
- Abstract machine semantics + midterm 1
- Computational effects
- Monadic semantics of computational effects
- Algebraic effects
- Effect handlers
- More advanced applications of effect handlers (transactions, generators, multithreading, pipes, ...) + midterm 2
- Polymorphism and existential types
- Type-and-effect systems
- Type-and-coeffect systems (incl. linear typing)
- Dependent types and program correctness
Assessment
Final grade is based on the sum of points from weekly homeworks, two midterms, and written exam.
The maximum possible points is 100. Maximum points according to assessment method:
- homeworks 14*1 points,
- midterms 2*25 points,
- exam 36 points.
The lecturer has the right to award students additional points for outstanding performance, which will be added to the exam points. A student can receive a maximum of 10 additional points.
Grading scale: 91%..100% -> A, 81%..90% -> B, 71%..80% -> C, 61%..70% -> D, 51%..60% -> E, 0%..50% -> F.
Midterms and exam
There are two written midterms during the semester:
- in week 7 (during the exercise class),
- in week 12 (during the exercise class).
Each midterm has one retake, the time of which will be agreed upon during the course.
There is a written exam during the exam period.
Both the midterms and exam consist of a pass/fail test part and a graded exercises part. The test part needs to be passed. In the exercises part, each correctly solved exercise awards a predetermined number of points, which are then added together.
The exercises part is open book, meaning that the use of personal paper materials is allowed. The use of computers or other electronic devices is not allowed.