The author gives an introductory overview of type theory for PhD students. He focuses on the use of type theory for compile-time checking of functional programs and on the use of types in proof assistants (theorem provers).

This book contains a thorough introduction to type theory, with information on polymorphic sets, subsets, monomorphic sets, and a full set of helpful examples. 

The book can be thought of as giving both a first and a second course in type theory. It begins with introductory material on logic and functional programming, and follow this by presenting the system of type theory itself, together with many examples.