Course PM

Introduction

In this course, you will learn the fundamentals of programming language theory, including formal semantics, type systems, and type soundness proofs. The course contains both theory and practice. During the course, you will also implement an interpreter for a typed functional language, as well as solving various theoretical exercises.

Learning Outcomes

After the course, the student will be able to

• Construct type soundness proofs
• Analyze type rules
• Analyze small-step and big-step operational semantics
• Implement an interpreter and a type checker for a typed functional language
• Apply untyped and simply typed lambda calculus with extensions

Teachers

Examiner and Course Responsible: 

• David Broman, dbro@kth.se

Examination

The student receives grade P if the following is fulfilled:

1. Active participation in seminars
2. Approved oral presentations at the seminars
3. Approved solutions to theoretical exercises
4. Approved submission and presentation of a software implementation

If the student cannot participate in a seminar, the student can do complementary work at another occasion.

Syllabus

The course syllabus is available in English or in Swedish.