Next: Computer Aided Formal Reasoning Up: Contents Previous: Support

Topics in Type Theory

This course is being held in room 5327, JCMB at 4 pm, Mondays and Wednesdays starting Monday 12th February 1996. It is arranged for the theory PG students, although others are of course welcome. The course aims to give an introduction to two central topics in the (syntactic) meta-theory of various type systems. In the first part of the course (Lectures 1-5; James McKinna), we focus on Barendregt's lambda-cube, and its generalisations known as Pure Type Systems, in order to study the problem of type-synthesis and type-checking; in the second (Lectures 6-9; Healf Goguen), we study proofs of strong normalisation using the technique of typed operational semantics, and discuss extensions of the basic functional framework of Part One to embrace inductive types and families of inductive types. There is a bibliography for the course, and there are lecture notes for the lectures on typed operational semantics and normalization for System F. Exercises will be given throughout, and the exam question will probably be a straight choice between a substantial exercise based on Part One or on Part Two.

Last updated on 23 April 1996 by Healfdene Goguen <>