FDD3024 Research preparation course in programming languages and formal methods

About the course

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.

Course intended learning outcomes

At the end of the course the student should be able to:

Apply several theories and methods covered in the course on sample problems of limited scope and size
Evaluate the suitability of a given theory/method within a given problem domain
Define and execute a first own research project within the students research area
Account for choice of approach
Relate own work to the state of the art in the area

Course organization

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 3-6 lectures.

Course examination

At the end of each period the course spans, a take-home exam is given over two days consisting of one problem set per module associated with that period. After handing in written solutions, 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.

Course modules

Module 1 (Period 4, spring 2026)

Topic: Lambda calculus, operational semantics, and types
Teachers: Karl Palmskog and Mohammad Ahmadpanah
Course literature: Practical Foundations for Programming Languages, 2nd edition by Robert Harper, PFPL for short, see abbreviated online edition

Module 2 (Period 4, spring 2026)

Topic: Formal models of concurrency, process algebras, execution traces, bisimulation, weak memory models, modal logics
Teachers: Mads Dam and Roberto Guanciale

Module 3 (Period 4, spring 2026)

Topic: Hoare logic, imperative program verification
Teachers: Karl Palmskog and Roberto Guanciale

Module 4 (Period 1, fall 2026)

Topic: Symbolic execution and abstract interpretation
Teachers: Roberto Guanciale and Musard Balliu

Module 5 (Period 1, fall 2026)

Topic: Security and information flow control
Teachers: Musard Balliu and Mohammad Ahmadpanah

Lecture Schedule for Period 4, 2026

Lecture	Module	Date	Time	Location	Topic	Slides
1	1	Apr 13	13:00	room 1537	Inductive rules, operational semantics, untyped lambda calculus	TBA
2	1	Apr 15	15:00	room 1537	Simply typed lambda calculus, type systems, ML	TBA
3	1	Apr 20	13:00	room 1537	Data types, abstract types, polymorphism, module systems	TBA
4	1	Apr 23	13:00	room 1537	Simple types, dependent types, theorem proving	TBA
5	2	Week 18	TBA	TBA	Concurrency	TBA
6	2	Week 18	TBA	TBA	Concurrency	TBA
7	2	Week 19	TBA	TBA	Concurrency	TBA
8	2	Week 19	TBA	TBA	Concurrency	TBA
9	2	Week 20	TBA	TBA	Concurrency	TBA
10	3	Week 20	TBA	TBA	Hoare logic	TBA
11	3	Week 20	TBA	TBA	Hoare logic	TBA
12	3	Week 20	TBA	TBA	Hoare logic	TBA

Lecture Resources

Lecture	Module	Resources
1	1	PFPL chapters 1-2 An Introduction to Inductive Definitions by Peter Aczel Untyped Lambda Calculus by Robert Harper A Structural Approach to Operational Semantics by Gordon Plotkin
2	1	PFPL chapter 4 A Sound Semantics for OCaml Light by Scott Owens A Verified Type System for CakeML by Tan et al.
3	1	PFPL chapters 9-11, 17, 44 A theory of type polymorphism in programming by Robin Milner Using dependent types to express modular structure by David B. MacQueen How to make ad-hoc polymorphism less ad hoc by Wadler and Blott
4	1	Church’s Type Theory by Stanford Encyclopedia of Philosophy A formulation of the simple theory of types by Alonzo Church Dependent types by Thorsten Altenkirch