Topics in Type Theory 1997

Type theory is an area of study that interacts with a variety of subjects in computer science. Type theoretical ideas such as polymorphism have been incorporated into modern programming languages such as Standard ML. Type theory is used in domain theory as an abstract language which captures the features of the intended models. Computer proof assistants such as LEGO are based on type-theoretic foundations.

The course discussed the motivations of type theory, and introduced a variety of increasingly sophisticated type theories, finishing with Luo's theory UTT. Important metatheoretic properties such as strong normalization, Church-Rosser and decidability of type checking were covered.

There is a bibliography for the course.

There is also information about Topics in Type Theory 1996.

Last updated on 12 February 1997 by Healfdene Goguen <>