Types
Principal lecturer: Dr Neel Krishnaswami
Taken by: Part II CST
Term: Michaelmas
Hours: 12
Format: In-person lectures
Suggested hours of supervisions: 3
Prerequisites: Computation Theory, Semantics of Programming Languages
Exam: Paper 8 Question 13, 13; Paper 9 Question 13, 13
Past exam questions, Moodle, timetable
Aims
The aim of this course is to show by example how type systems for programming languages can be defined and their properties developed, using techniques that were introduced in the Part IB course on Semantics of Programming Languages. The emphasis is on type systems for functional languages and their connection to constructive logic.
Lectures
- Introduction. The role of type systems in programming languages. Review of rule-based formalisation of type systems. [1 lecture]
- Propositions as types. The Curry-Howard correspondence between intuitionistic propositional calculus and simply-typed lambda calculus. Inductive types and iteration. Consistency and termination. [2 lectures]
- Polymorphic lambda calculus (PLC). PLC syntax and reduction semantics. Examples of datatypes definable in the polymorphic lambda calculus. Type inference. [3 lectures]
- Monads and effects. Explicit versus implicit effects. Using monadic types to control effects. References and polymorphism. Recursion and looping. [2 lectures]
- Continuations and classical logic. First-class continuations and control operators. Continuations as Curry-Howard for classical logic. Continuation-passing style. [2 lectures]
- Dependent types. Dependent function types. Indexed datatypes. Equality types and combining proofs with programming. [2 lectures]
Objectives
At the end of the course students should
- be able to use a rule-based specification of a type system to carry out type checking and type inference;
- understand by example the Curry-Howard correspondence between type systems and logics;
- understand how types can be used to control side-effects in programming;
- appreciate the expressive power of parametric polymorphism and dependent types.
Recommended reading
* Pierce, B.C. (2002). Types and programming
languages. MIT Press.
Pierce, B. C. (Ed.) (2005). Advanced Topics in Types and
Programming Languages. MIT Press.
Girard, J-Y. (tr. Taylor, P. and Lafont, Y.) (1989). Proofs
and types. Cambridge University Press.