Types

Lecturer: Dr A.M. Pitts (ap@cl.cam.ac.uk)

No. of lectures: 8  

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

Introduction.

The role of type systems in programming languages.

Type inference.

ML-style polymorphism. Principal types and the Hindley-Damas-Milner theorem.

Polymorphic lambda calculus.

Syntax and reduction semantics. Statement of strong normalisation property. Examples of datatypes definable in the polymorphic lambda calculus.

Further topics.

Subtyping. Dependent types. The propositions-as-types paradigm.

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.