In this entry, we first give an overview of the most important aspects of intuitionistic type theory—a kind of “extended abstract”. It is meant for a reader who is already somewhat familiar with the theory. Section 2 on the other hand, is meant for a reader who is new to intuitionistic type theory but familiar with traditional logic, including propositional and predicate logic, arithmetic, and set theory. Here we informally introduce several aspects which distinguishes intuitionistic type theory from these traditional theories. In Section 3 we present a basic version of the theory, close to Martin-Löf’s first published version from 1972. The reader who was intrigued by the informality of Section 2 will now see in detail how the theory is built up. Section 4 then presents a number of important extensions of the basic theory. In particular, it emphasizes the central role of inductive (and inductive-recursive) definitions. Section 5 introduces the underlying philosophical ideas including the theory of meaning developed by Martin-Löf. While Section 5 is about philosophy and foundations, Section 6 gives an overview of mathematical models of the theory. In Section 7 finally, we describe several important variations of the core Martin-Löf “intensional” theory described in Section 3 and 4.