Type Systems for Programming Languages

Course Information

Lecture time:

• Monday, 11:00 - 12:50, room 144.
• Thursday, 14:00 - 15:50, room 145.

Notes:

The notes

induction

derivation.sty

Assessed Course Work:

Description:

Although the topic of the course sits within the area of theoretical computer science, the course itself does not intend to focus on theoretical aspects. Rather, it aims to focus on design, to show how to set up a formal system; proofs of properties are only shown as illustration. As such, the course introduces students into formalized systems, and the focus of attention is on presentation of a couple of existing approaches. New systems and languages will be introduced, but these will serve mainly to set the context of the course.

Over the past years, this course attracted a small number of students, facilitating a friendly and highly interactive way of teaching. The chosen format for the lectures is that with an integrated tutorial, which allows for focussing on exercises and particular problems, as well as detailed discussions with the student group on the 'why' and 'how' of what appears during the course.

Past students have highly appreciated the course, and did very well in the exam.

Objective

The aim of this course is to lay out in detail the design of type assignment systems for (functional) programming languages and focus on the importance of a sound theoretical framework, in order to be able to reason about the properties of a typed program. Students will study and compare a variety of systems and languages.

Prerequisites

None; students who have taken Models of Computation in the second year will have seen the techniques used in the course.

Contents

The course sets of with the presentation of the Lambda Calculus, on which most functional languages are based. We will introduce the Curry Type Assignment System for this calculus, for which we show that

• types are respected by reduction;
• there exists a notion of principality on types, i.e. all types for a program can be constructed from the 'principal' type;
• type assignment is decidable.

We will show how to extend the language and the system of types in order to deal with Polymorphism. To this end, Combinator Systems are introduced as a slight extension of LC. In order to study how to deal with Recursion, the language of CS is extended to allow for recursive definitions, and we will discuss ways of typing this extension. We will then look at Milner's basic ML system, and show that, in this calculus, a solution is present for all the issues discussed separately before.

A disadvantage of ML is that it is, syntactically, very distant from actual programming languages, and it is not easy to see that all properties shown for ML translate to the 'real' languages. In particular, definitions of functions by 'cases' (Pattern Matching) are not present in ML. In order to come to a formal notion of types that relates more closely to actual programming languages, we introduce Term Rewriting Systems, which are much closer to actual programs, and show that we can obtain much of the desired properties.

We will look at abstract data types and recursive types, and compare and confront the various approaches that exist.

To conclude, we will have a brief visit to the intersection type system, and discuss its relation with semantics.