Abstract: I will give an overview of the field of Homotopy Type Theory. This relatively new field of mathematics is based on a realization that the formal logical system of dependent type theory can be interpreted in various homotopy-theoretic settings. After briefly discussing type theory, I will sketch the idea of its homotopical interpretation and its connection to higher category theory. In the last part of the talk, I will highlight some recent results.