SEM230 Types and Semantics for Programming Languages (20cr, Sem 1 and 2)
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.
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.
3 hour written examination and continuous assessment.
Co-Requisites: none, but attendence of SEM241 a serious advantage
Max/Min Course Numbers: unspecified
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