View the course on
GitHub
This course at KTH introduces theory, methods, and tools that are prerequisites for research in the areas of programming languages and formal methods. The course awards 10 ECTS credits and the examiner is Mads Dam.
At the end of the course the student should be able to:
The course consists of five modules given by members of faculty and postdocs at the KTH Department of Theoretical Computer Science over a full term = two periods. Each module consists of 2-6 lectures.
The course has two forms of examination: homeworks and take-home exams.
Each module has a homework problem set where a written solution must be handed in that is graded pass/fail based on demonstrated effort to solve problems; solutions need not be correct. The aim of the homeworks to help students prepare for the take-home exam.
At the end of each period the course spans, a take-home exam is given consisting of one problem set per module associated with that period. Students must book a slot to present and discuss their solutions with a teacher, who will then grade each problem set pass/fail. A student must get a pass on all problem sets to pass the course.
Module 1 (Period 4, spring 2026)
Module 2 (Period 4, spring 2026)
Module 3 (Period 4, spring 2026)
Module 4 (Period 1, fall 2026)
Module 5 (Period 1, fall 2026)
| Lecture | Module | Date | Time | Location | Topic | Slides |
|---|---|---|---|---|---|---|
| 1 | 1 | Apr 13 | 13:00 | room 1537 | Inductive rules, operational semantics, untyped lambda calculus | Lecture 1 |
| 2 | 1 | Apr 15 | 15:00 | room 1537 | Simply typed lambda calculus, type systems, ML | Lecture 2 |
| 3 | 1 | Apr 20 | 13:00 | room 1537 | Data types, polymorphism, abstract types, module systems | Lecture 3 |
| 4 | 1 | Apr 23 | 13:00 | room 1537 | Simple types, dependent types, theorem proving | Lecture 4 |
| 5 | 2 | Apr 28 | 10:00 | room 4423 | Concurrency, Executions, Interleaving | Lecture 5 |
| 6 | 2 | Apr 29 | 10:00 | room 1537 | Process Algebra, CCS, pi-calculus | Lecture 6 |
| 7 | 2 | May 4 | 15:00 | room 4423 | Weak Memory Models | Lecture 7 |
| 8 | 2 | May 6 | 10:00 | room 1537 | Modal and Temporal Logics | Lecture 8 |
| 9 | 2 | May 12 | 10:00 | room 4423 | Modal and Temporal Logics | Lecture 9 |
| 10 | 3 | May 18 | 13:00 | room 1537 | Basic Hoare logic | Lecture 10 |
| 11 | 3 | May 19 | 10:00 | Teknikringen 31: 1320 | Practical Hoare logic | Lecture 11 |
| Lecture | Module | Date | Time | Location | Topic | Slides | |
|---|---|---|---|---|---|---|---|
| 12 | 4 | Oct 13 | 13:00 | room 1537 | Symbolic execution | Lecture 1 | Lean 4 model |
| 13 | 4 | Oct 15 | 13:00 | room 1537 | Symbolic execution for procedures, arrays, function pointers | Lecture 2 |