Course pages 2015–16

# Types

**Principal lecturer:** Prof Andrew Pitts**Taken by:** Part II**Past exam questions**

No. of lectures: 12

suggested hours of supervisions: 3

Prerequisite courses: Computation Theory, Semantics of Programming Languages

## Aims

The aim of this course is to show by example how type systems for
programming languages can be defined and their properties developed,
using techniques that were introduced in the Part IB course on * Semantics of Programming Languages*. The emphasis is on type systems
for functional languages and their connection to constructive logic.

## Lectures

**Introduction.**The role of type systems in programming languages. Review of rule-based formalisation of type systems. [1 lecture]**ML polymorphism.**ML-style polymorphism. Principal type schemes and type inference. [2 lectures]**Polymorphic reference types.**The pitfalls of combining ML polymorphism with reference types. [1 lecture]**Polymorphic lambda calculus (PLC).**Explicit versus implicitly typed languages. PLC syntax and reduction semantics. Examples of datatypes definable in the polymorphic lambda calculus. [3 lectures]**Dependent types.**Dependent function types. Pure type systems. System F-omega. [2 lectures]**Propositions as types.**Example of a non-constructive proof. The Curry-Howard correspondence between intuitionistic second-order propositional calculus and PLC. The calculus of Constructions. Inductive types. [3 lectures]

## Objectives

At the end of the course students should

- be able to use a rule-based specification of a type system to carry out type checking and type inference;
- understand by example the Curry-Howard correspondence between type systems and logics;
- appreciate the expressive power of parametric polymorphism and dependent types.

## Recommended reading

* Pierce, B.C. (2002). *Types and programming languages*. MIT
Press.

Pierce, B. C. (Ed.) (2005). *Advanced Topics in Types and
Programming Languages*. MIT Press.

Girard, J-Y. (tr. Taylor, P. & Lafont, Y.) (1989). *Proofs and
types*. Cambridge University Press.