Formalizing mathematics and dependent types

The theme of the Colloquium will be " Formalizing Mathematics and Dependent Types ". Colloquium guests are specialists in the implementation or theory of proof assistants, type theory, higher-order category notions, and mathematicians who use these systems to represent proofs on computers. One of the questions addressed will be to what extent the recent rapprochement between the formalism of dependent types and the notions of homotopy and higher-order categories can be relevant to the actual formalization of mathematics.