To provide students with an understanding of the basis of the theory of types as used in Programming Languages, as well as the basics of Programming Languages semantics.

We introduce the simply typed calculus, the ML typing system (let-polymorphism, type inference, principal types) and a basic system for subtyping. We show the important connection between types and propositions, the Curry-Howard correspondence. Optional topics, in the first part of the course include the second order (polymorphic) lambda calculus and a static type system for objects. In the second half of the course we develop semantics in the form of structured operational semantics. We also introduce denotational semantics.

2 lectures per week, with an extra hour organised to discuss exercises.

A. Pitts "Types" slides and lecture notes and "Semantics of Programming Languages" lecture notes.

G. Winskel "The Formal Semantics of Programming Languages -- An Introduction" MIT Press, Foundations of Computing Series.

J-Y. Girard, Y. Lafont and P. Taylor "Proofs and Types", Cambridge University Press.

Last update: 30th March 1997

Go to the School of Computer Science Home Page (http://www.cs.bham.ac.uk/)