Seminars, Modules, and Exercises

Seminars

The course is divided into 3 modules. Each module starts with a seminar and ends with a seminar. 

• Seminar 1: Course Introduction and Introduction to Module 1.
  Time and place: Ada, KTH Kista, Friday, December 6, 2024, 10 am - 12 pm (noon).
• Seminar 2: Presentation of solutions to Module 1 and Introduction to Module 2.
  Time and place: Ada, KTH Kista, Tuesday, March 4, 2025, 9 am - 12 pm (noon).
• Seminar 3: Presentation of solutions to Module 2 and Introduction to Module 3.
  Time and place: TBD
• Seminar 4: Presentation of solutions to Module 3. Course ending.
  Time and place: TBD

Module Exercises

Module 1: Operational semantics and the lambda calculus

The main topics for module 1 are: 

• Small-step and big-step operational semantics
• Untyped lambda calculus
• Fundamental typed functional programming

Exercises for module 1:

• Perform all the tasks and exercises in this PDF-document.
• You can use the following example files when solving the above exercises. 

Reading guidelines for module 1:

• Read the TAPL Chapter 1 (as an introduction) and Chapter 2 (to make sure that you have the mathematical background).
• Read TAPL Chapters 3, 4, 5, 6, and 7 carefully.
• Read the paper Natural Semantics by Kahn (1987). See the literature page for a link.
• Read sections 2.1-2.3 of Simon Peyton Jones' book The Implementation of Functional Programming Languages (1987) 

Be prepared to give a presentation of some of the topics that you have read, or to present some of your solutions. Who will present what will be announced approximately 1 weeks before seminar 2 (when I know who have actually submitted exercises).

Module 2: Typed lambda calculus with extensions

• Type rules
• Simply typed lambda calculus
• Type soundness proofs
• Semantics for let bindings, pairs, tuples, records, sums, and lists
• References and exceptions

Exercises for module 2:

• Perform all the tasks and exercises in this PDF-document.
• You should base your solutions on the implementation that you did in module 1.

Reading guidelines for module 2:

• Read TAPL Chapters 8, 9, 10, 11, 12, 13, and 14 carefully.

Module 3: Subtyping and Polymorphism

• Subtype polymorphism
• Parametric polymorphism
• Ad-hoc polymorphism
• Structural and nominal type systems
• Gradual typing

Exercises for module 3:

• Perform all the tasks and exercises in this PDF-document.
• You should base your solutions on the implementation that you did in module 1.

Reading guidelines for module 3:

• Read sections 1.1, 1.2, and 1.3 of the paper On understanding types, data abstraction, and polymorphism by Cardelli and Wegner (1985).
• Read the paper How to make ad-hoc polymorphism less ad hoc by Wadler and Blott (1989).
• Read sections 1 and 2 of the paper Gradual Typing for Functional Languages by Siek and Taha (2006).
• Read the paper (focus on semantic formalization)  Gradually typed symbolic expressions by Broman and Siek (2018).
• Read TAPL Chapters 15, 16, 19, and 23 carefully.