Programming in Martin-Löf's Type Theory
Bengt Nordström, Kent Petersson, Jan M. Smith
From the Preface:
"This book describes diﬀerent type theories (theories of types, polymorphic and monomorphic sets, and subsets) from a computing science perspective. It is intended for researchers and graduate students with an interest in the foundations of computing science, and it is mathematically self-contained."