Principles of Programming Languages
- ÕIS data: LTAT.03.027, 6 ECTS.
- Lectures: Thursdays 16:15-18:00 in Delta-2045
- Exercise classes: Fridays 16:15-18:00 in Delta-2047
- Lecture slides, exercise sheets, weekly info: Moodle
- Language English.
- Contact: 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 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 study common program logics and how to use them to specify and verify the correctness of state-manipulating programs. We will then investigate type-and-effect systems and dependent types as a means to encode correctness specifications in types. To this end we, will explore both functional correctness properties, and properties concerning side-effects and their behaviour.
Weekly topics
- Introduction and untyped lambda calculus
- Simply typed lambda calculus
- Subtyping
- Operational semantics
- Properties of operational semantics
- Denotational semantics
- Recursion + midterm 1
- Computational effects
- Monadic semantics
- Algebraic effects and effect handlers
- Other control operators
- Polymorphism + midterm 2
- Type-and-effect systems
- Dependently typed lambda calculus
- Program logics and dependent types
- Modal and linear type systems
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 test part and exercises part. 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.