Course Description

Type systems play a large role in languages such as Haskell and ML, but also languages such as Java and C#. In this course we focus on higher-order functional languages, and investigate type systems for these languages, and extensions to them. In addition, there is a wealth of literature about type and effect systems that borrow vocabulary and techniques from these type systems to compute statically information from programs that can be used to optimise and validate others aspects of the programs. Among these one can find strictness analysis, control flow analysis, binding-time analysis, pattern match analysis and dozens of others.

The goal of this course is to introduce many such analyses for higher-order languages, to introduce polyvariance as a means of context-sensitive analysis of functional programs, to consider how laziness may effect such analyses and how subeffecting and subtyping may be used to increase precision.

Much of your work in this course is under your own control: I am open to suggestions. Want to analyze the Java type system for your presentation, want to consider contracts for Ruby. Anything is open to discussion. Make the most of it.

-- JurriaanHage - 16 Aug 2011