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.