head 1.2; access; symbols; locks; strict; comment @# @; 1.2 date 98.06.09.18.04.07; author da; state Exp; branches; next 1.1; 1.1 date 98.06.09.18.03.40; author da; state Exp; branches; next ; desc @@ 1.2 log @Removed silly header. @ text @
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.