*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 is 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.