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
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
There is a bibliography for the course.
There is also information about Topics in Type