Students of formal logic or foundations of mathematics often first encounter the phrase “type theory” in the context of Bertrand Russell’s ramified theory of types. But type theory is in fact a diverse class of formal systems, many of which are currently undergoing rapid and fruitful development. This workshop will be devoted to certain theoretical aspects and practical implementations of dependent type theory - notably developed by Swedish logician, philosopher, and computer scientist Per Martin-Löf - which has been shown to have surprising and powerful connections to abstract fields of mathematics such as category theory and more recently homotopy theory. Dependent type theory can serve as: a foundation for constructive/intuitionistic mathematics; a logic and functional programming language under the propositions-as-types paradigm or Curry-Howard correspondence; and even as a basis for formal semantics of natural language. More generally, dependent type theory as a logic offers an alternative to classical first order predicate calculus in its various applications.