Types

Lecturer: Dr P.M. Sewell (pes20@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. [1 lecture]

ML-style polymorphism.

ML-style polymorphism. Type inference. Principal types and the Hindley-Damas-Milner theorem. Implementation. [3 lectures]

Second-order polymorphism.

Polymorphic lambda calculus. Syntax and reduction semantics. Statement of strong normalisation property. Examples of datatypes definable in the polymorphic lambda calculus. [3 lectures]

Further topics.

Abstract data types and existential types. Subtyping. [1 lecture]

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.