Latest update May 18, 2001
To avoid spam, all mail addresses on this page have the "@" replaced by "#".
Always under construction!
Spring 2001
Slides for the lecture 01-05-04 (dvi format).
Advanced Type Systems is a ?? cu Ph.D. level course at the Dept. of Computer Engineering (IDt), Mälardalen University. The course leaders are Björn Lisper, e-mail bjorn.lisper#mdh.se, phone 021-151709, and Mikael Sandberg, e-mail mikael.sandberg#mdh.se, phone 021-103177.
Except for an introductory lecture, the format will be seminars that are given by the participants themselves. Thus, different particpants will present different papers, on a round-robin basis. It is expected that all participants read the material in advance for each seminar.
The number of credits will be decided later, probably individually, on the basis of attendance and presentations made. There will be no examination apart from that.
Type systems are important in programming languages. Type checking is a simple way to ensure at compile-time that a program that compiles is free from certain errors. An extension of type checking, type inference, derives types in a program where types are not explicitly given. Certain modern functional languages, like ML and Haskell, use type inference. Type inference also opens the road to using type systems for program analysis: nonstandard types can express properties of programs, and type inference will then deduce whether programs have these properties by inferring the corresponding types for them.
In this course we will try to give a both broad and deep coverage of modern type systems: which kinds of type systems there are, and what we can do with them.
The usefulness of type system motivates their study. Also, type systems is a fairly hot topic in programming language research. Thus, in order to understand many research papers, it is necessary to have a good working knowledge of type systems.
To give the participants a good knowledge of modern type systems, what they can be used for, and different kinds of type inference.
We will start with the following, and add some more papers later.
The following excerpts provide background material for the first lecture:
The following papers will be scheduled later:
Basic Polymorphic Typechecking, Luca Cardelli, Science of Computer Programming, vol 8, 1987, p147-172. Slides for the lecture (pdf format)
A Theory of Type Polymorphism, Robin Milner, Journal of Computer and System Sciences, vol 17, 1978, p348-375. Slides for the lecture (postscript and dvi)
Principal Type-Schemes for Function Programs, Luis Damas and Robin Milner, Conference Record of the Ninth Annual {ACM} Symposium on Principles of Programming Languages, 1982
A Practical Soft Type System for Scheme, Andrew Wright and Robert Cartwright, ACM Transactions on Programming Languages and Systems, Vol. 19, 1997, p87-152
Type Inclusion Constraints and Type Inference, Alexander Aiken and Edward L. Wimmers, Proc. FPCA, 1993, 31-41. Slides for the lecture (postscript format, full size and 4-up)
On Understanding Types, Data Abstraction, and Polymorphism, Luca Cardelli and Peter Wegner, ACM Computing Surveys, Vol. 17, 1985, 471-522
A Region Inference Algorithm, Mads Tofte, ACM Transactions on Programming Languages and Systems, Vol. 20, 1998, p724-767
Type Classes in Haskell, Cordelia V. Hall, Kevin Hammond, Simon L. Peyton Jones, Philip L. Wadler, ACM Transactions on Programming Languages and Systems, Vol 18, 1996, pp 109-138. Slides for the lecture (postscript and dvi).
Cayenne - a language with dependent types, Lennart Augustsson, ACM SIGPLAN International Conference on Functional Programming, 1998, pp. 239-25. Slides for the lecture (postscript and dvi).