SEM230 Types and Semantics for Programming Languages (20cr, Sem 1 and 2)

Status: Closed
Staff: Valeria de Paiva
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.
Module Description
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.
Assessment: 3 hour written examination and continuous assessment.
Faculty: Science
Co-Requisites: none, but attendence of SEM241 a serious advantage
Pre-Requisites: none
Max/Min Course Numbers: unspecified
Key Texts
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.
Course Notes

Maintained by
Last update: 30th March 1997
Go to the School of Computer Science Home Page (