Type Theory and Formal Proof - Nederpelt, Rob (Technische Universiteit Eindhoven, The Netherlands) a Geuvers, Herman (Radboud Universiteit Nijmegen)

Type theory is a fast-evolving field at the crossroads of logic, computer science and mathematics. This book provides a gentle step-by-step introduction in the art of formalizing mathematics on the basis of type theory. It is suitable for a broad audience, ranging from undergraduate students to researchers.