Type Systems for Programming Languages

Type systems prevent illegal program behavior and provide important feedback to programmers. In this course, we will study the various flavors of type systems in detail. In particular, we will investigate:

  • dynamic type checking
  • operational semantics
  • soundness of type systems
  • reference types, exception types
  • type inference
  • polymorphism
  • subtyping
  • dependent types
  • implementation of type systems

We will study type systems both from a theoretical standpoint and from a pragmatic standpoint by looking at existing programming languages with sophisticated type systems.

Course Information



Course Type

IV4 / 6 CPs.
We will freely mix different lecturing styles: classroom lectures, interactive discussion, longer programming task, paper reading.


Dr. Sebastian Erdweg, Prof. Dr.-Ing. Mira Mezini




For lecture via TUCaN. For assignments via WebLab.

Lecture times

Monday, 14:25-16:05, S101/A3

Tuesday, 16:15-17:55, S101/A3

First lecture on Tuesday, October 15.


March 10, 2014, 13.00-15.00, S206/030

Homework assignments

There will be homework assignments on a regular basis. Handing in assignments is optional, but a bonus for the final grade can be obtained. The maximal bonus is a 0.5 improvement of the final grade.

We use the online learning platform WebLab for publishing assignments, collecting hand-ins, and communicating feedback on the hand-ins. To register an account with WebLab, visit register with your Full Name as user name (e.g., SebastianErdweg). After you are logged in, you can enroll in for this course here

Course material

The prime resource for this course is the text book “Types and Programming Languages” by Benjamin Pierce. I highly recommend obtaining a copy. You can obtain a substituted copy here:

Other resources such as slides or code can be found here: