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. Formalising 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 lecture]
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 books
* 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.
