Computation and Reasoning: A Type Theory for Computer Science by Zhaohui Luo

This book develops a type theory, studies its properties, and explains its uses in computer science. The book focuses in particular on how the study of type theory may offer a powerful and uniform language for programming, program specification and development, and logical reasoning.