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.

Seminars

The course consists of a number of seminars. During these seminars, the students present solutions to exercises and problems. Please see the page seminars for more details.

Literature

The following is the recommended course book:

• Benjamin C. Pierce, Types and Programming Languages, The MIT Press, 2002

Besides the main course book, a number of scientific articles and papers will also be part of the course literature. See the literature page to the left for more information.

Policy for Plagiarism

Note that all forms of cheating and plagiarism will be reported. Please see KTH's policy for handling plagiarism. 

Syllabus

The course syllabus is available in English.