Type Theory and Formal Proof An Introduction

A gentle introduction for graduate students and researchers in the art of formalizing mathematics on the basis of type theory.