Computer Laboratory – Course material 2007

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

Types

Lecturer: Professor A.M. Pitts

No. of lectures: 8

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

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.

Lectures

Introduction. The role of type systems in programming languages. Formalizing 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. Syntax and reduction semantics. Examples of datatypes definable in the polymorphic lambda calculus. Applications. [2 lectures]
Further topics. The Curry-Howard correspondence as a source of type systems. Dependent types. [2 lectures]

Objectives

At the end of the course students should

appreciate how type systems can be used to constrain or describe the dynamic behaviour of programs
be able to use a rule-based specification of a type system to infer typings and to establish type soundness results
appreciate the expressive power of the polymorphic lambda calculus

Recommended reading

* Pierce, B.C. (2002). Types and programming languages. MIT Press.
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.

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