Type Systems for Programming Languages

Module aims

In this module you will study in detail the design of type assignment systems for 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. You will also study and compare the types systems of various modern functional and object-oriented programming languages.

Learning outcomes

Upon successful completion of this module you will be able to:

• evaluate the relative merits of dynamic and static typing for functional, imperative, and objected oriented languages
• formalise type systems and prove properties such as decidability, soundness, and completeness
• describe and implement algorithms for type inference and type checking
• describe and formalise selected type system extensions required to support modern programming language features
• demonstrate advanced features of modern statically-typed programming lanaguges through small applications

Module syllabus

• Review of Lambda calculus
• Curry type assignment and principal types
• Recursion and polymorphism
• Type checking vs type inference
• System F
• Extensions for practical type inference, including data types, type classes,  type constraints and coercion
• System F_C
• Subtypes and subtype inference
• Advanced topics, e.g. higher-rank types, dependent types and ownership types

Teaching methods

The emphasis in this module is on combining theory with practice. There will be traditional lectures showing how type systems can be formalised and reasoned about and these will be interspersed with in-class discussions backed up with unassessed, formative, exercises designed to reinforce your understanding of the taught material. There will be additional laboratory exercises where you will get to explore advanced typing features and implement type checking/ inference algorithms, representative of those in modern statically-typed programming language compilers. Graduate Teaching Assistants will be on hand to support the laboratory exercises.

An online service will be used as a discussion forum for the module.

Assessments

There will be one assessed coursework containing both theoretical and practical components, which accounts for 20% of the module mark. The remaining 80% of the marks come from a written examination which will test both theoretical and practical aspects of the subject.

There will be written feedback on the assessed coursework exercise. Graduate Teaching Assistants will also provide verbal feedback as part of the administration of the laboratory exercises.   

Module leaders

Dr Steffen van Bakel