** Next:** VLSI Design
** Up:** Michaelmas Term 2002: Part
** Previous:** Specification and Verification I
** Contents**

##

Types

*Lecturer: Prof. A.M. Pitts*
(`amp12@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]

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

Pierce, B.C. (2002). *Types and Programming Languages*. MIT Press.

** Next:** VLSI Design
** Up:** Michaelmas Term 2002: Part
** Previous:** Specification and Verification I
** Contents**
*Christine Northeast*

*Wed Sep 4 14:43:05 BST 2002
*