Types

Lecturer: Dr A.M. Pitts (ap@cl.cam.ac.uk)

No. of lectures: 8

Prerequisite courses: Semantics of Programming Languages, Foundations of Functional Programming

Aims

The aim of this course will be to show how the mathematical formalism introduced in the Part IB course on Semantics of Programming Languages can be applied to the task of specifying and reasoning about type systems for programming languages.

Lectures

• Introduction. The role of type systems in programming languages. Safety via types. Formalising type systems. [1 lecture]

• ML polymorphism. ML-style polymorphism. Principal type schemes and type inference. [3 lectures]

• Polymorphic reference types. The pitfalls of combining ML polymorphism with reference types. [1 lecture]

• Second-order polymorphism. Polymorphic lambda calculus. Syntax and reduction semantics. Statement of strong normalisation property. Examples of datatypes definable in the polymorphic lambda calculus. [3 lectures]

Objectives

At the end of the course students should

• appreciate how type systems can be used to constrain the dynamic behaviour of programs

• be able to use a rule-based specification of a type system to show, in simple cases, that a given expression is, or is not typeable

• be able to describe, in outline, a particular type inference algorithm involving parametric polymorphism

Recommended books

Cardelli, L. (1997). Type Systems. In CRC Handbook of Computer Science and Engineering. CRC Press.
Cardelli, L. (1987). Basic Polymorphic Typechecking. Science of Computer Programming, vol. 8, pp. 147-172.
Girard, J-Y. (tr. Taylor, P. & Lafont, Y.) (1989). Proofs and Types. Cambridge University Press.